proposition: Lemma prID A B mu : \P_[mu] A = \P_[mu] [predI A & B] + \P_[mu] [predI A & predC B].
proof: Proof. rewrite {1}/pr (psumID B); first by apply/summable_pr. congr (_ + _); apply/eq_psum => x; rewrite !inE -!topredE /=; by rewrite mulrA -natrM mulnb andbC. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum