proposition: Lemma jtype_choiceMixin A B n : choiceMixin (P_ n ( A , B )).
proof: Proof. apply (PcanChoiceMixin (@jtype_choice_pcancel A B n)). 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