fact: Hypothesis V_dom_by_W : P |- V << W.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals Lra mathcomp(Rstruct reals) ssrR realType_ext Reals_ext Ranalysis_ext logb ln_facts fdist entropy channel_code channel divergence conditional_divergence variation_dist pinsker