proposition: Lemma chargeD nu (A B : set T) : measurable A -> measurable B -> nu (A `\` B) = nu A - nu (A `&` B).
proof: Proof. move=> mA mB. rewrite (chargeDI nu mA mB) addeK// fin_numE 1?gt_eqF 1?lt_eqF//. - by rewrite ltey_eq fin_num_measure//; exact:measurableI. - by rewrite ltNye_eq fin_num_measure//; exact:measurableI. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral