proposition: Lemma type_fun_type A n (_ : n != O) (P : P_ n ( A )) a : ((type.f P) a)%:R = n%:R * type.d P a.
proof: Proof. case: P => /= d f d_f; by rewrite d_f mulRCA mulRV ?INR_eq0' // mulR1. 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