proposition: Lemma type_ffunP A n (P Q : P_ n.+1 ( A )) : (forall c, type.d P c = type.d Q c) -> P = Q.
proof: Proof. move=> H. destruct P as [d1 f1 H1]. destruct Q as [d2 f2 H2]. rewrite /= in H. apply/type_eqP => /=. apply/eqP/ffunP => a. apply/val_inj/INR_eq. move: {H}(H a); rewrite H1 H2 eqR_mul2r //. apply/invR_neq0; by rewrite INR_eq0. 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