proposition: Lemma Pr_fdist_prod_of_rV (A : finType) n (P : {fdist 'rV[A]_n.+1}) (E : {set A}) (F : {set 'rV[A]_n}) : Pr (fdist_prod_of_rV P) (E `* F) = Pr P [set x : 'rV[A]_n.+1 | ((x ``_ ord0) \in E) && ((rbehead x) \in F)].
proof: Proof. rewrite /Pr (eq_bigr (fun x => fdist_prod_of_rV P (x.1, x.2))); last by case. rewrite [in LHS](eq_bigl (fun a => (a.1 \in E) && (a.2 \in F))); last first. by move=> [a b]; rewrite !inE. rewrite -[in LHS](pair_big (mem E) (mem F) (fun x1 x2 => fdist_prod_of_rV P (x1, x2))) /=. rewrite [in RHS](eq_bigl (fun x : 'rV_n.+1 => (x ``_ ord0 \in E) && (rbehead x \in F))); last first. by move=> v; rewrite !inE. rewrite -(big_rV_cons_behead _ (mem E) (mem F)) /=. by apply eq_bigr => a aE; apply eq_bigr => v _; rewrite fdist_prod_of_rVE. 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