proposition: Lemma set_vals_prod_vals_id vals i : set_vals (prod_vals vals) vals i = vals i.
proof: Proof. rewrite !ffunE; by case: (i \in _) (vals i). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba