proposition: Lemma Pr_fdistX (A B : finType) (P : {fdist A * B}) (E : {set A}) (F : {set B}) : Pr (fdistX P) (F `* E) = Pr P (E `* F).
proof: Proof. rewrite /Pr !big_setX exchange_big /=; apply eq_bigr => b _. by apply eq_bigr => a _; rewrite fdistXE. 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