proposition: Lemma bound_card_jtype : #| P_ n (A , B) | <= expn n.+1 (#|A| * #|B|).
proof: Proof. rewrite -(card_ord n.+1) mulnC expnM -2!card_ffun cardE /enum_mem. apply (@leq_trans (size (map (@ffun_of_jtype A B n) (Finite.enum (jtype_finType A B n))))). by rewrite 2!size_map. rewrite cardE. apply: uniq_leq_size. rewrite map_inj_uniq. rewrite -enumT; by apply enum_uniq. move=> [c f Hf Hc] [c1 f1 Hf1 Hc1] /= ?; subst f1. by apply/jtype_eqP => /=. move=> /= x. case/mapP => t Ht Hx. subst x. destruct t as [c f Hf cf] => /=. apply/mapP. by exists f. 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