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