proposition: Lemma set_vals_tl (v : prod_types) vs i : i \notin I -> set_vals v vs i = vs i.
proof: Proof. rewrite !ffunE; by case: (i \in I) (v i). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba