proposition: Lemma Pr_setTX F : Pr P ([set: A] `* F) = Pr (P`2) F.
proof: Proof. rewrite /Pr big_setX /= exchange_big; apply eq_bigr => a aE. by rewrite fdist_sndE /=; 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