simp [Nat.sub_succ']
case succ.h.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ x ^ (n - i - 1) = x ^ (n - Nat.succ i)
no goals