proposition: Lemma measureUfinl A B : measurable A -> measurable B -> mu A < +oo -> mu (A `|` B) = mu A + mu B - mu (A `&` B).
proof: Proof. by move=> *; rewrite setUC measureUfinr// setIC [mu B + _]addeC. 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)