∀ {f : ℝ → ℝ} {a b : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Ioo a b) →
      DifferentiableOn ℝ f (Set.Ioi b) →
        (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioi b, 0 ≤ deriv f x) → IsMinOn f (Set.Ioi a) b