fact: Definition d : {fdist A * B * C} := fdistX (fdistA (fdistX (fdistA P)))`2.
imports: mathcomp(all_ssreflect ssralg matrix) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba jfdist_cond