proposition: Lemma pr_or A B mu : \P_[mu] [predU A & B] = \P_[mu] A + \P_[mu] B - \P_[mu] [predI A & B].
proof: Proof. apply/eqP; rewrite eq_sym subr_eq [in X in _==X]addrC; apply/eqP. rewrite (prID _ B) -addrA -pr_or_indep => [x|]. by rewrite !inE => /andP[]. congr (_ + _); apply/eq_pr => x; rewrite !inE -!topredE /=. by apply/orb_id2r => /negbTE ->; rewrite andbT. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum