proposition: Lemma sum_pow_euler n k: \sum_(i<n) i ^k.+1 = \sum_(i<k.+1) 'Eu(k.+1,i) * 'C(n+i,k.+2).
proof: Proof. move: k; elim :n. move => k;rewrite big_ord0 big1 // => [] [i lin] _ /=. by rewrite bin_small ?muln0 // add0n leqW //. move => n IHn k; rewrite big_ord_recr /= IHn euler_sum_pow - big_split /=. by apply: eq_bigr => i _; rewrite - mulnDr (addSn n) binS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)