∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → E},
  IntervalIntegrable f μ a b → IntervalIntegrable g μ a b → IntervalIntegrable (fun x => f x - g x) μ a b