proposition: Lemma measureU2 A B : measurable A -> measurable B -> mu (A `|` B) <= mu A + mu B.
proof: Proof. move=> ? ?; rewrite -bigcup2inE bigcup_mkord. rewrite (le_trans (@content_sub_additive _ _ _ mu _ (bigcup2 A B) 2%N _ _ _))//. by move=> -[//|[//|[|]]]. by apply: bigsetU_measurable => -[] [//|[//|[|]]]. by rewrite big_ord_recr/= big_ord_recr/= big_ord0 add0e. 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)