fact: Definition type_eq A n (t1 t2 : P_ n ( A )) := match t1, t2 with | type.mkType _ f1 _, type.mkType _ f2 _ => f1 == f2 end.
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