∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → E} {K a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      f a = 0 → (∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ K * ‖f x‖) → ∀ x ∈ Set.Icc a b, f x = 0