proposition: Corollary genfun_length n : \sum_(s : 'S_n) 'X^(length s) = \prod_(0 <= i < n) \sum_(0 <= j < i.+1) 'X^j : {poly int}.
proof: Proof. case: n => [|n]. rewrite (big_pred1_id _ _ (i := 1%g)); first last. by move=> s; rewrite !permS0 /= eq_refl. by rewrite addr0 length1 expr0 big_mkord big_ord0. rewrite (reindex _ (onW_bij _ (prods_codesz_bij n))) /=. under eq_bigr => i _ do rewrite (length_permcd (codeszP _)) // ?size_codesz //. rewrite /prods_codesz -big_enum /=. rewrite -(big_map (@cdval _) xpredT (fun i : seq nat => 'X^(sumn i))). elim: n => [/= | n]. by rewrite enum_codeszE /index_iota !big_seq1 /= addn0. move: (n.+1) => {}n. rewrite /index_iota !enum_codeszE big_flatten big_map -/enum_codesz. rewrite !subn0 -{2}addn1 iotaD add0n [iota 0 n.+1]lock /=. rewrite big_cat /= big_seq1 {2}[(0 :: iota 1 n)%N]lock /= => <-. rewrite big_distrr /=; apply eq_bigr => i _. rewrite big_distrl /= big_map; apply eq_bigr => j _. by rewrite -sumn_rev rev_rcons /= sumn_rev exprD mulrC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr