proposition: Lemma semi_additiveW : mu set0 = 0 -> semi_additive -> semi_additive2.
proof: Proof. move=> mu0 amx A B mA mB + AB; rewrite -bigcup2inE bigcup_mkord. move=> /(amx (bigcup2 A B))->. - by rewrite !(big_ord_recl, big_ord0)/= adde0. - by move=> [|[|[]]]//=. - by move=> [|[|i]] [|[|j]]/= _ _; rewrite ?(AB, setI0, set0I, setIC) => -[]. 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)