fact: Definition prod_vars : {RV P -> prod_types types I} := fun u => prod_vals I (vals_at u).
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba