proposition: Lemma set_val_tl i (v : types i) vs j : i <> j -> set_val v vs j = vs j.
proof: Proof. rewrite ffunE => nij; case: Nat.eq_dec => ij //; elim nij; exact: ord_inj. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba