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

State before:
k : ℕ
⊢ fzn (-↑(k + 1)) = 2 * k + 1
Tactic:
rfl
State after:
no goals