proposition: Lemma sum_pow n k: \sum_(i<n) i ^k = \sum_(i<k.+1) 'Sj(k,i) * 'C(n,i.+1).
proof: Proof. elim:n => [| n Hrec]. rewrite big_ord0 big1 //; case => i Hi _. by have ->: 'C(0,i.+1) = 0 by []; rewrite muln0. rewrite big_ord_recr /= - sum_nbsurj Hrec - big_split //. by apply: eq_bigr =>i _ /=; rewrite - mulnDr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)