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

State before:
a m n : Nat
⊢ a % (m * n) % n = a % n
Tactic:
rw [Nat.mul_comm, mod_mul_mod_left]
State after:
no goals