proposition: Lemma card_nu : #|\nu^{B}( P )| <= expn n.+1 (#|A| * #|B|).
proof: Proof. apply: (leq_trans _ (bound_card_jtype A B n)). apply subset_leq_card; by apply/subsetP. 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