proposition: Lemma type_empty1 n : #|A| = 0 -> #|P_ n(A)| = 0.
proof: Proof. move=> A0; apply eq_card0; case=> d ? ?. move: (fdist_card_neq0 d); by rewrite A0. 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