proposition: Lemma Pr_fdist_snd (A B : finType) (P : {fdist A * B}) (E : {set B}) : Pr P`2 E = Pr P (T`* E).
proof: Proof. rewrite /Pr (eq_bigr (fun x => P (x.1, x.2))); last by case. rewrite [in RHS](eq_bigl (fun x => true && (x.2 \in E))); last first. by move=> [a b]; rewrite !inE. rewrite -[in RHS](pair_big xpredT (mem E) (fun x1 x2 => P (x1, x2))) /=. under eq_bigr do rewrite fdist_sndE. by rewrite exchange_big. 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