Theorem: ipow_neg_succ (HOLFloat/Common.lean)

State before:
r : ℝ
i : ℕ
⊢ r ^ -[i+1] = (r ^ Nat.succ i)⁻¹
Tactic:
simp_all only [zpow_negSucc]
State after:
no goals