proposition: Lemma integral_measure_add_nnsfun d (T : measurableType d) (R : realType) (m1 m2 : {measure set T -> \bar R}) (D : set T) (mD : measurable D) (f : {nnsfun T >-> R}) : (\int[measure_add m1 m2]_(x in D) (f x)%:E = \int[m1]_(x in D) (f x)%:E + \int[m2]_(x in D) (f x)%:E)%E.
proof: Proof. rewrite /measureD integral_measure_sum_nnsfun// 2!big_ord_recl/= big_ord0. by rewrite 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