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

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