proposition: Lemma integralB_EFin d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (f1 f2 : T -> R) (mD : measurable D) : mu.-integrable D (EFin \o f1) -> mu.-integrable D (EFin \o f2) -> (\int[mu]_(x in D) ((f1 x)%:E - (f2 x)%:E) = (\int[mu]_(x in D) (f1 x)%:E - \int[mu]_(x in D) (f2 x)%:E))%E.
proof: Proof. move=> if1 if2; rewrite (integralD_EFin mD if1); last first. by rewrite (_ : _ \o _ = (fun x => - (f2 x)%:E))%E; [exact: integrableN|by []]. by rewrite -integralN//; exact: integrable_add_def. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun