proposition: Lemma PrX_snd F : \sum_(a in A) Pr P ([set a] `* F) = Pr (P`2) F.
proof: Proof. rewrite -Pr_setTX /Pr big_setX; apply: eq_big => a; first by rewrite !inE. by rewrite big_setX /= 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