proposition: Lemma occ_co_occ : forall a b, N(a, b| ta, tb) = (JType.f V) a b.
proof: Proof. move: Htb => Htb' x0 y0 ; rewrite /shell inE in Htb'. apply/eqP; move: y0; apply/forallP; move: x0; apply/forallP; exact Htb'. 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