proposition: Lemma pr_split B A mu : \P_[mu] A = \P_[mu] B * \P_[mu, B] A + \P_[mu] (predC B) * \P_[mu, predC B] A.
proof: Proof. suff h A' B': \P_[mu] [predI A' & B'] = \P_[mu] B' * \P_[mu, B'] A'. by rewrite (prID _ B); congr (_ + _); apply/h. rewrite /prc mulrCA; have [] := eqVneq (\P_[mu] B') 0; last first. by move=> nzPB'; rewrite divff // mulr1. move=> zPB'; rewrite zPB' invr0 !mulr0; apply/eq0_pr. move=> x mux; move/pr_eq0: zPB' => /(_ x) h; rewrite !inE. by apply/negP=> /andP[_ /h] /dinsuppP. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum