proposition: Lemma set_vals_hd vs2 (v : prod_types) vs1 i : i \in I -> set_vals v vs1 i = set_vals v vs2 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