proposition: Lemma prod_vars_inter (I J : {set 'I_n}) vals i u : i \in I -> i \in J -> set_vals (prod_vars I u) vals i = set_vals (prod_vars J u) vals i.
proof: Proof. move=> *; by rewrite !set_vals_prod_vals. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba