proposition: Lemma type_choice_pcancel A n : pcancel (@type.f A n) (@type_choice_f A n).
proof: Proof. case=> d t H /=. destruct n. by move: (no_0_type H). rewrite /type_choice_f /=; f_equal. move: (ffun_of_fdist H) => H'. destruct Sumbool.sumbool_of_bool as [e|e]; last first. by rewrite H' in e. congr Some. set d1 := fdist_of_ffun _. suff ? : d1 = d by subst d; congr type.mkType; apply boolp.Prop_irrelevance. apply fdist_ext => /= a; by rewrite ffunE H. 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