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

State before:
a b : ℕ
⊢ fnnn (a, b) = tri (a + b) + a
Tactic:
rfl
State after:
no goals