∀ {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
  x₀ < x →
    ContDiffOn ℝ (↑n + 1) f (Set.Icc x₀ x) →
      ∃ x' ∈ Set.Ioo x₀ x,
        f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x =
          iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial