feat(data/zmod/basic): some lemmas about coercions (#12571)

The names here are in line with `zmod.nat_coe_zmod_eq_zero_iff_dvd` and `zmod.int_coe_zmod_eq_zero_iff_dvd` a few lines above.

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

src/data/zmod/basic.lean

@@ -430,6 +430,37 @@ begin
   rw [zmod.nat_coe_eq_nat_coe_iff, nat.modeq_zero_iff_dvd],
 end
 
+lemma val_int_cast {n : ℕ} (a : ℤ) [fact (0 < n)] : ↑(a : zmod n).val = a % n :=
+begin
+  have hle : (0 : ℤ) ≤ ↑(a : zmod n).val := int.coe_nat_nonneg _,
+  have hlt : ↑(a : zmod n).val < (n : ℤ) := int.coe_nat_lt.mpr (zmod.val_lt a),
+  refine (int.mod_eq_of_lt hle hlt).symm.trans _,
+  rw [←zmod.int_coe_eq_int_coe_iff', int.cast_coe_nat, zmod.nat_cast_val, zmod.cast_id],
+end
+
+lemma nat_coe_zmod_eq_iff (p : ℕ) (n : ℕ) (z : zmod p) [fact (0 < p)] :
+  ↑n = z ↔ ∃ k, n = z.val + p * k :=
+begin
+  split,
+  { rintro rfl,
+    refine ⟨n / p, _⟩,
+    rw [val_nat_cast, nat.mod_add_div] },
+  { rintro ⟨k, rfl⟩,
+    rw [nat.cast_add, nat_cast_zmod_val, nat.cast_mul, nat_cast_self, zero_mul, add_zero] }
+end
+
+lemma int_coe_zmod_eq_iff (p : ℕ) (n : ℤ) (z : zmod p) [fact (0 < p)] :
+  ↑n = z ↔ ∃ k, n = z.val + p * k :=
+begin
+  split,
+  { rintro rfl,
+    refine ⟨n / p, _⟩,
+    rw [val_int_cast, int.mod_add_div] },
+  { rintro ⟨k, rfl⟩,
+    rw [int.cast_add, int.cast_mul, int.cast_coe_nat, int.cast_coe_nat, nat_cast_val,
+      zmod.nat_cast_self, zero_mul, add_zero, cast_id] }
+end
+
 @[push_cast, simp]
 lemma int_cast_mod (a : ℤ) (b : ℕ) : ((a % b : ℤ) : zmod b) = (a : zmod b) :=
 begin