no goals
a b n : Nat
⊢ a * b % n = a % n * (b % n) % n
conv => lhs; rw [
  ← mod_add_div a n, ← mod_add_div b n, Nat.add_mul, Nat.mul_add, Nat.mul_add,
  Nat.mul_assoc, Nat.mul_assoc, ← Nat.mul_add n, add_mul_mod_self_left,
  Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left]