fact: Definition rvar_choice (A : eqType) (X : {RV P -> A}) := X fdist_choice.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba