proposition: Lemma jtype_count_pcancel A B n : pcancel (@jtype_pickle A B n) (@jtype_unpickle A B n).
proof: Proof. move=> V. rewrite /jtype_unpickle /jtype_pickle /=. destruct V as [[c Anot0] f Hf H]. destruct Sumbool.sumbool_of_bool; last by rewrite Anot0 in e. case/card_gt0P : (e) => a Ha. move: (fdist_card_neq0 (c a)) => Bnot0. destruct Sumbool.sumbool_of_bool; last by rewrite Bnot0 in e0. rewrite pickleK. set d1 := chan_of_jtype _ _ _. have ? : d1 = Channel1.mkChan c Anot0. apply/Channel1.chan_star_eq. by rewrite boolp.funeqE => a1; apply/fdist_ext => b /=; 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