proposition: Lemma jtype_choice_pcancel (A B : finType) n : pcancel (@JType.f A B n) (@jtype_choice_f A B n).
proof: Proof. case=> d f Hf H /=. rewrite /jtype_choice_f /=. destruct d as [d Hd]. destruct Sumbool.sumbool_of_bool; last by rewrite Hd in e. destruct Sumbool.sumbool_of_bool; last first. exfalso. case/card_gt0P : e => a Ha. move: e0. by rewrite (fdist_card_neq0 (d a)). set d1 := chan_of_jtype _ _ _. set d2 := Channel1.mkChan d Hd. have d12 : d1 = d2. apply/Channel1.chan_star_eq. rewrite boolp.funeqE => /= a; apply/fdist_ext => b; by rewrite ffunE H. destruct Sumbool.sumbool_of_bool; last by rewrite Hf in e1. congr Some; by apply/jtype_eqP => /=. 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