∀ {f f' : ℝ → ℝ} {a b l : ℝ},
  a < b →
    Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
      Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l) →
        (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) → ∃ c ∈ Set.Ioo a b, f' c = 0