theorem intervalIntegral.integral_mono_on_of_le_Ioo {μ : MeasureTheory.Measure ℝ} {a b : ℝ} {f g : ℝ → ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) [MeasureTheory.NoAtoms μ] (h : ∀ x ∈ Set.Ioo a b, f x ≤ g x) : ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

To put just after integral_mono_on.