proposition: Lemma type_card_neq0 n : 0 < #|A| -> 0 < #|P_ n.+1(A)|.
proof: Proof. case/card_gt0P => a _. apply/card_gt0P. have [f Hf] : [finType of {f : {ffun A -> 'I_n.+2} | \sum_(a in A) f a == n.+1}]. exists [ffun a1 => if pred1 a a1 then Ordinal (ltnSn n.+1) else Ordinal (ltn0Sn n.+1)]. rewrite (bigD1 a) //= big1; first by rewrite ffunE eqxx addn0. move=> p /negbTE Hp; by rewrite ffunE Hp. exists (@type.mkType _ _ (fdist_of_ffun Hf) _ (fdist_of_ffun_prop Hf)). by rewrite inE. 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