no goals
a b n : Int
⊢ a * b % n = a % n * (b % n) % n
conv => lhs; rw [
  ← emod_add_ediv a n, ← emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
  Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
  ← Int.mul_assoc, add_mul_emod_self]