proposition: Lemma ffun_of_fdist (A : finType) n (d : {fdist A}) (t : {ffun A -> 'I_n.+2}) (H : forall a : A, d a = INR (t a) / INR n.+1) : (\sum_(a in A) t a)%nat == n.+1.
proof: Proof. suff : INR (\sum_(a in A) t a) == INR n.+1 * \sum_(a | a \in A) d a. by move/eqP; rewrite (FDist.f1 d) mulR1 => /INR_eq/eqP. apply/eqP. transitivity (INR n.+1 * (\sum_(a|a \in A) INR (t a) / INR n.+1)). by rewrite -big_distrl -big_morph_natRD mulRCA mulRV ?mulR1 // INR_eq0'. congr (_ * _); exact/eq_bigr. 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