Theorem: HTPI.mul_mod_mod_eq_mul_mod (HTPILib/Chap7.lean)

State before:
m a b : ℕ
⊢ a % m * (b % m % m) % m = a % m * (b % m) % m
Tactic:
rw [Nat.mod_mod]
State after:
no goals