Differential-to-integral comparison

If f is continuous on [0,T], differentiable on (0,T) with f' ≤ B and B continuous on [0,T], then f T ≤ f 0 + ∫_0^T B. No regularity of f' is needed.

theorem AVenhance.Infra.FullTheorem.Separation.le_add_integral_of_deriv_le {f f' B : ℝ → ℝ} {T : ℝ} (hT : 0 ≤ T) (hf : ContinuousOn f (Set.Icc 0 T)) (hd : ∀ s ∈ Set.Ioo 0 T, HasDerivAt f (f' s) s) (hB : ContinuousOn B (Set.Icc 0 T)) (hle : ∀ s ∈ Set.Ioo 0 T, f' s ≤ B s) : f T ≤ f 0 + ∫ (s : ℝ) in 0..T, B s