proposition: Lemma type_empty2 : #|P_ 0(A)| = 0.
proof: Proof. apply eq_card0; case=> d f Hf. exfalso. by move/no_0_type in Hf. 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