exact mul_le_mul_of_nonneg_right (hC _ hx') (abs_nonneg _)
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| ≤ C * |(x - x₀) ^ (n + 1)|
no goals