∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          ∀ {C : ℝ}, (∀ x ∈ interior D, deriv f x < C) → ∀ x ∈ D, ∀ y ∈ D, x < y → f y - f x < C * (y - x)