fact: Definition set_vals : prod_types -> univ_types -> univ_types := Eval hnf in set_vals'.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba