proposition: Lemma pr_dunit E x : \P_[dunit x] E = (E x)%:R :> R.
proof: Proof. rewrite /pr (psum_finseq (r := [:: x])) //. move=> y; rewrite !inE dunit1E [x==_]eq_sym. by case: (y =P x) => //; rewrite mulr0 eqxx. by rewrite big_seq1 dunit1E eqxx mulr1 ger0_norm ?ler0n. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum