proposition: Lemma additive2P : mu set0 = 0 -> semi_additive mu <-> additive2 mu.
proof: Proof. move=> mu0; rewrite -semi_additive2E; split; first exact: semi_additiveW. rewrite semi_additiveE semi_additive2E => muU A Am Atriv n. elim: n => [|n IHn]; rewrite ?(big_ord_recr, big_ord0) ?mu0//=. rewrite muU ?IHn//=; first by apply: bigsetU_measurable. rewrite -bigcup_mkord -subset0 => x [[/= m + Amx] Anx]. by rewrite (Atriv m n) ?ltnn//=; exists x. 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)