proposition: Lemma measure0 : mu set0 = 0.
proof: Proof. have /[!big_ord0] ->// := @measure_semi_additive _ _ _ mu (fun=> set0) 0%N. exact: trivIset_set0. 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)