proposition: Lemma charge_semi_additiveW nu : nu set0 = 0 -> measure.semi_additive nu -> semi_additive2 nu.
proof: Proof. move=> nu0 anu A B mA mB + AB; rewrite -bigcup2inE bigcup_mkord. move=> /(anu (bigcup2 A B)) ->. - by rewrite !(big_ord_recl, big_ord0)/= adde0. - by move=> [|[|[]]]//=. - move=> [|[|i]] [|[|j]]/= _ _ //. + by rewrite AB => -[]. + by rewrite setI0 => -[]. + by rewrite setIC AB => -[]. + by rewrite setI0 => -[]. + by rewrite set0I => -[]. + by rewrite set0I => -[]. + by rewrite setI0 => -[]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral