fact: Definition mutual_info_dist (P : {fdist A * B}) := `H P`1 + `H P`2 - `H P.
imports: mathcomp(all_ssreflect all_algebra) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy jfdist_cond