proposition: Lemma content_ring_sigma_additive : sigma_sub_additive mu -> semi_sigma_additive mu.
proof: Proof. move=> mu_sub A Am Atriv UAm. suff <- : \sum_(i <oo) mu (A i) = mu (\bigcup_n A n) by exact: is_cvg_nneseries. by apply/eqP; rewrite eq_le mu_sub// ?content_ring_sup_sigma_additive. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)