proposition: Lemma ge0_integral_fsum (A : set I) : finite_set A -> \int[mu]_(x in D) (\sum_(k \in A) f k x) = \sum_(k \in A) \int[mu]_(x in D) f k x.
proof: Proof. move=> fs; rewrite fsbig_finite//= -ge0_integral_sum//. by apply: eq_integral => x xD; rewrite fsbig_finite. 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