proposition: Lemma f1 : \sum_(g in {ffun M -> 'rV[A]_n}) f g = 1.
proof: Proof. under eq_bigr do rewrite ffunE /=. rewrite -(bigA_distr_bigA (fun _ v => P `^ n v)) /=. rewrite [RHS](_ : _ = \prod_(m0 : M | xpredT m0) 1); last by rewrite big1. by apply eq_bigr => _ _; rewrite (FDist.f1 (P `^ n)). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix perm) Reals Lra Classical mathcomp(Rstruct classical_sets) ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq joint_typ_seq channel channel_code