Theorem: Nat.mod_mul_mod (Algdata/Init/Nat.lean)

State before:
a b n : Nat
⊢ a * b % n = (n * (a / n) + a % n) * b % n
Tactic:
conv => lhs; rw [←Nat.div_add_mod a n]
State after:
no goals

State before:
a b n : Nat
⊢ (n * (a / n) + a % n) * b % n = (n * (a / n * b) + a % n * b) % n
Tactic:
rw [Nat.right_distrib, Nat.mul_assoc]
State after:
no goals

State before:
a b n : Nat
⊢ (n * (a / n * b) + a % n * b) % n = a % n * b % n
Tactic:
rw [Nat.add_comm,Nat.add_mul_mod_self_left]
State after:
no goals