proposition: Lemma pr_or_indep (A B : pred T) (mu : {distr T / R}) : (forall x, x \in A -> x \notin B) -> \P_[mu] [predU A & B] = \P_[mu] A + \P_[mu] B.
proof: Proof. move=> dsj; rewrite /pr -psumD; try solve [ by apply/summable_pr | by move=> x; rewrite mulr_ge0 ?ler0n ]. apply/eq_psum=> x /=; rewrite -mulrDl -!topredE /= -natrD. case/boolP: (A x) => Ax; case/boolP: (B x) => Bx //=. by move/dsj: Ax; rewrite -topredE /= Bx. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum