proposition: Lemma eq0_prc A B mu : (forall x, x \in dinsupp mu -> x \in B -> x \notin A) -> \P_[mu, B] A = 0.
proof: Proof. move=> h; rewrite /prc eq0_pr ?mul0r // => x /h {h} /orb_idl. by rewrite negb_and /= => <-; rewrite orbAC orbN. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum