no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.42710
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ (x : ℝ), x ∈ Icc 0 1 → HasDerivWithinAt f (f' x) (Icc 0 1) x
bound : ∀ (x : ℝ), x ∈ Ico 0 1 → ‖f' x‖ ≤ C
⊢ ‖f 1 - f 0‖ ≤ C
simpa only [sub_zero, mul_one] using
  norm_image_sub_le_of_norm_deriv_le_segment' hf bound 1 (right_mem_Icc.2 zero_le_one)