Mul emod and coprime

Stream: Is there code for X?

[Xavier Xarles]

I need the following lemmas, which I already proved (the second with a may be too long proof).

import Mathlib.Data.Int.GCD

lemma mul_emod_eq_mul_mod_right {m n k : ℤ} (i : ℤ) (H : m % n = k % n):
    (m * i) % n = (k * i) % n := by rw[Int.mul_emod,Int.mul_emod k,H]

lemma mul_emod_cancel_if_coprime (n m: ℕ)(co: n.Coprime m)(a b:ℤ)(h:(a*n)%m=(b*n)%m): a%m=b%m := by
    have eq1 := mul_emod_eq_mul_mod_right (n.gcdA m) h
    have eq2 : 1= n * n.gcdA m + m* n.gcdB m := by rw [← Nat.gcd_eq_gcd_ab,co]; exact rfl;
    have eq3 := sub_eq_iff_eq_add.mpr eq2
    rw [Int.mul_assoc a _ _, eq3.symm] at eq1
    rw [Int.mul_assoc b _ _, eq3.symm] at eq1
    rw [Int.mul_sub,mul_one] at eq1
    rw [Int.mul_sub,mul_one] at eq1
    rw [Int.sub_emod,Int.sub_emod b] at eq1
    rw [Int.mul_left_comm,Int.mul_emod_right] at eq1
    rw [Int.mul_left_comm,Int.mul_emod_right] at eq1
    simp_all only [sub_zero, dvd_refl, Int.emod_emod_of_dvd, add_sub_cancel_right]