simp
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x✝¹ : ℝ
x✝ : x✝¹ ∈ Ioo a b
⊢ 1 ≠ 0
no goals