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

State before:
q : ℚ
⊢ fqn q = fnnn (fzn q.num, q.den)
Tactic:
rfl
State after:
no goals