fact: Definition ffun_of_jtype A B n (i : P_ n ( A , B )) := let: JType.mk _ f _ _ := i in f.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types