Integer residues as natural numbers

Main results

• Int.natCast_toNat_emod: the nonnegative integer residue survives a round trip through Nat.

Bounds on natural residues use Mathlib's existing Int.natMod_lt.

References

Adapted from Index.lean at anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. The existing Exact Triangle hashing client now uses these shared facts.

theorem Int.natCast_toNat_emod {p : ℕ} (hp : 0 < p) (u : ℤ) : ↑(u % ↑p).toNat = u % ↑p

Casting the natural Euclidean residue back to Int preserves its value for a positive modulus.