proposition: Lemma prod_vars_pair (I J : {set 'I_n}) : [disjoint I & J] -> RV_equiv (prod_vars (I :|: J)) [% prod_vars I, prod_vars J].
proof: Proof. move=> Disj. esplit. exact: cancel_both_disjoint. move=> u /=. congr pair; apply/ffunP => i; apply prod_vals_eq => Hi; rewrite set_vals_prod_vars ?ffunE //; by rewrite inE Hi ?orbT. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba