refine' pow_ne_zero _ _
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ (x - y) ^ n ≠ 0
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x - y ≠ 0