Theorem: HTPI.mod_mod_def (HTPILib/Chap8Part2.lean)

State before:
m n a : ℕ
⊢ mod_mod m n a = (a % m, a % n)
Tactic:
rfl
State after:
no goals