proposition: Lemma rsum_rmul_rV_pmf_tnth (R : realType) A n k (P : fdist R A) : \sum_(t : 'rV[ 'rV[A]_n]_k) \prod_(m < k) (P `^ n) t ``_ m = 1.
proof: Proof. transitivity (\sum_(j : {ffun 'I_k -> 'rV[A]_n}) \prod_(m : 'I_k) P `^ _ (j m)). rewrite (reindex_onto (fun p : 'rV_k => [ffun i => p ``_ i]) (fun x : {ffun 'I_k -> 'rV_n} => \row_(i < k) x i)) //=; last first. by move=> f _; apply/ffunP => /= k0; rewrite ffunE mxE. apply eq_big => //. - by move=> v /=; apply/esym/eqP/rowP => i; rewrite mxE ffunE. - by move=> i _; apply eq_bigr => j _; rewrite ffunE. rewrite -(bigA_distr_bigA (fun m => P `^ _)) /= big_const. by rewrite iter_mulr FDist.f1 expr1n mulr1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext