proposition: Lemma set_vals_id (v : prod_types) vs : set_vals v (set_vals v vs) = set_vals v vs.
proof: Proof. apply/ffunP => i. case/boolP: (i \in I) => [/set_vals_hd | /set_vals_tl ->]; exact. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba