rw [norm_iteratedFDeriv_eq_norm_iteratedDeriv, iteratedDeriv_pow]
case h
n i : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
case h
n i : ℕ
x : ℝ
⊢ ‖(fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)