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

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