proposition: Lemma measureD A B : measurable A -> measurable B -> mu A < +oo -> mu (A `\` B) = mu A - mu (A `&` B).
proof: Proof. move=> mA mB mAoo. rewrite (measureDI mA mB) addeK// fin_numE 1?gt_eqF 1?lt_eqF//. - by rewrite (le_lt_trans _ mAoo)// le_measure // ?inE//; exact: measurableI. - by rewrite (lt_le_trans _ (measure_ge0 _ _)). 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)