proposition: Lemma pr_pred1 mu x : mu x = \P_[mu] (pred1 x).
proof: Proof. rewrite /pr (psum_finseq (r := [:: x])) // => [y|]. by rewrite !inE; case: (y =P x); rewrite ?(mul0r, eqxx). by rewrite big_seq1 /= eqxx mul1r ger0_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum