proposition: Lemma type_co_occ a b : ((type.f P) a * (JType.f V) a b = N(a, b | ta, tb) * N(a | ta))%nat.
proof: Proof. by rewrite occ_co_occ mulnC (type_numocc Hta a). Qed.
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