proposition: Lemma prod_dist_inde_rv_vec (A : finType) (P : {fdist A}) n (X : A -> R) (Y : {RV (P `^ n) -> R}) x y : `Pr[ ([% (fun v => X v ``_ ord0) : {RV (P`^n.+1) -> _}, (fun v => Y (rbehead v) : _ )]) = (x, y) ] = `Pr[ ((fun v => X v ``_ ord0) : {RV (P`^n.+1) -> _}) = x ] * `Pr[ ((fun v => Y (rbehead v)) : {RV (P`^n.+1) -> _}) = y ].
proof: Proof. have /= := @prod_dist_inde_rv _ _ P (P `^ n) _ _ X Y x y. rewrite !pr_eqE -!fdist_prod_of_fdist_rV. rewrite (_ : [set x0 | _] = (finset (X @^-1 x)) `* (finset (Y @^-1 y))); last first. by apply/setP => -[a b]; rewrite !inE /= xpair_eqE. rewrite Pr_fdist_prod_of_rV (_ : [set x0 | _] = (finset (X @^-1 x)) `*T); last first. by apply/setP => a; rewrite !inE. rewrite Pr_fdist_prod_of_rV1 (_ : [set x0 | _] = T`* (finset (Y @^-1 y))); last first. by apply/setP => a; rewrite !inE. move=> Hinde. apply: eq_trans. apply: eq_trans; last exact: Hinde. by congr Pr; apply/setP => v; rewrite !inE xpair_eqE. by rewrite Pr_fdist_prod_of_rV2; congr (Pr _ _ * Pr (P `^ n.+1) _); apply/setP => v; 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