fact: Variables (A : prod_types types e) (B : prod_types types f) (C : prod_types types g).
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba