proposition: Lemma type_numocc ta (Hta : ta \in T_{P}) a : N(a | ta) = type.f P a.
proof: Proof. move: Hta. rewrite in_set. move/forallP/(_ a)/eqP. destruct P as [d f H] => /= Htmp. apply/INR_eq/esym; move: Htmp. rewrite H eqR_mul2r //. by apply/invR_neq0; rewrite INR_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum perm) mathcomp(matrix) mathcomp(Rstruct) Reals ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist proba entropy num_occ channel_code channel typ_seq