proposition: Lemma type_enumP A n : Finite.axiom (@type_enum A n).
proof: Proof. destruct n. case=> d t H /=; by move: (no_0_type H). case=> d t H /=. move: (ffun_of_fdist H) => H'. have : Finite.axiom (enum [finType of { f : {ffun A -> 'I_n.+2} | (\sum_(a in A) f a)%nat == n.+1}]). rewrite enumT; by apply enumP. move/(_ (@exist {ffun A -> 'I_n.+2} (fun f => \sum_(a in A) f a == n.+1)%nat t H')) => <-. rewrite /type_enum /= /type_enum_f /= count_map. by apply eq_count. 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