proposition: Lemma type_counting n : #| P_ n ( A ) | <= expn (n.+1) #|A|.
proof: Proof. rewrite -(card_ord n.+1) -card_ffun /=. rewrite cardE /enum_mem. apply (@leq_trans (size (map (@ffun_of_type A n) (Finite.enum (type_finType A n))))). by rewrite 2!size_map. rewrite cardE. apply: uniq_leq_size. rewrite map_inj_uniq //. move: (enum_uniq (type_finType A n)). by rewrite enumT. case=> d f Hd [] d2 f2 Hd2 /= ?; subst f2. have ? : d = d2 by apply/fdist_ext => a; rewrite Hd Hd2. subst d2; congr type.mkType; exact: boolp.Prop_irrelevance. move=> /= f Hf; by rewrite mem_enum. 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