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

State before:
k : ℕ
⊢ fzn ↑k = 2 * k
Tactic:
rfl
State after:
no goals