∀ {g g' : ℝ → ℝ} {a l : ℝ},
  ContinuousWithinAt g (Set.Ici a) a →
    (∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Ioi a, 0 ≤ g' x) → Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a