proposition: Lemma integral_measure_add d (T : measurableType d) (R : realType) (m1 m2 : {measure set T -> \bar R}) (D : set T) (mD : measurable D) (f : T -> \bar R) : (forall x, D x -> 0 <= f x)%E -> measurable_fun D f -> (\int[measure_add m1 m2]_(x in D) f x = \int[m1]_(x in D) f x + \int[m2]_(x in D) f x)%E.
proof: Proof. move=> f0 mf; rewrite /measureD ge0_integral_measure_sum// 2!big_ord_recl/=. by rewrite big_ord0 adde0. 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