proposition: Lemma type_ext A n (t1 t2 : P_ n ( A )) : type.f t1 = type.f t2 -> t1 = t2.
proof: Proof. case: t1 t2 => d1 f1 H1 /= [] d2 f2 H2 /= f1f2. subst f2. suff ? : d1 = d2 by subst d2; congr type.mkType; exact: boolp.Prop_irrelevance. apply fdist_ext => /= a; by rewrite H1 H2. 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