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

State before:
a m n : Nat
⊢ a % (m * n) % m = a % m
Tactic:
conv =>
  rhs;
  rw [←Nat.div_add_mod a (m*n), Nat.add_comm, Nat.mul_assoc]
  simp
State after:
no goals