proposition: Lemma set_val_hd i (v : types i) vs : set_val v vs i = v.
proof: Proof. rewrite ffunE eq_dec_refl -Eqdep_dec.eq_rect_eq_dec //; exact: ord_eq_dec. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba