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

State before:
m a b : ℕ
⊢ a % m * b % m = a * b % m
Tactic:
rewrite [mul_comm, mul_mod_mod_eq_mul_mod, mul_comm]
State after:
m a b : ℕ
⊢ a * b % m = a * b % m

State before:
m a b : ℕ
⊢ a * b % m = a * b % m
Tactic:
rfl
State after:
no goals