proposition: Lemma prc_sum A mu : 0 < \P_[mu] A -> psum (fun x => \P_[mu, A] (pred1 x)) = 1.
proof: Proof. move=> gt0_pE; rewrite psumZr ?(invr_ge0, ge0_pr) //. rewrite (eq_psum (F2 := (fun x => (A x)%:R * mu x))); last first. by rewrite divff // gt_eqF. move=> x /=; rewrite /pr (psum_finseq (r := [:: x])) ?big_seq1 //=. move=> y; rewrite !inE; case: (y == x) => //=. by rewrite mul0r eqxx. by rewrite !inE eqxx -topredE ger0_norm ?mulr_ge0 ?ler0n. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum