proposition: Lemma type_choiceMixin A n : choiceMixin (P_ n ( A )).
proof: Proof. apply (PcanChoiceMixin (@type_choice_pcancel A n)). 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