proposition: Lemma Pr_XsetT E : Pr P (E `* [set: B]) = Pr (P`1) E.
proof: Proof. rewrite [in RHS]/Pr; under [in RHS]eq_bigr do rewrite fdist_fstE. rewrite /Pr big_setX /=; apply: eq_bigr => a aE. by apply: eq_bigl => b; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist