proposition: Lemma set_vals_prod_vars vals u i : i \in I -> set_vals (prod_vars u) vals i = vars i u.
proof: Proof. move=> Hi; by rewrite set_vals_prod_vals // ffunE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba