use n - i, Nat.descFactorial n i
n i : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k
case h
n i : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)