proposition: Lemma PrX_fst E : \sum_(b in B) Pr P (E `* [set b]) = Pr (P`1) E.
proof: Proof. rewrite -Pr_XsetT /Pr big_setX /= [in RHS]exchange_big /=; apply: eq_big => b. by rewrite !inE. by move=> _; rewrite big_setX /= exchange_big big_set1. 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