proposition: Lemma fdist_of_ffun_prop (A : finType) n (f : {ffun A -> 'I_n.+2}) (Hf : (\sum_(a in A) f a)%nat == n.+1) : forall a : A, (fdist_of_ffun Hf) a = INR (f a) / INR n.+1.
proof: Proof. by move=> a; rewrite ffunE. 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