proposition: Lemma positive_negative0 nu P N : nu.-positive_set P -> nu.-negative_set N -> forall S, measurable S -> nu (S `&` P `&` N) = 0.
proof: Proof. move=> [mP posP] [mN negN] S mS; apply/eqP; rewrite eq_le; apply/andP; split. apply: negN; first by apply: measurableI => //; exact: measurableI. by apply/setIidPl; rewrite -setIA setIid. rewrite -setIAC. apply: posP; first by apply: measurableI => //; exact: measurableI. by apply/setIidPl; rewrite -setIA setIid. 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