proposition: Lemma euler_sum_pow k n : k ^n.+1 = \sum_(i<n.+1) 'Eu(n.+1,i) * 'C(k+i,n.+1).
proof: Proof. elim:n; first by rewrite big_ord_recl big_ord0 mul1n // addn0 bin1 // addn0. move => n Hrec. rewrite big_ord_recl // addn0 eulern0 mul1n. transitivity (\sum_(i < n.+2) i.+1 * 'Eu(n.+1, i) * 'C(k + i, n.+2) + (\sum_(i < n.+1) (n.+1-i) * 'Eu(n.+1, i) * 'C(k + i.+1, n.+2)));last first. rewrite big_ord_recl // addn0 eulern0 mul1n - addnA -big_split /=. by congr (_ + _); apply: eq_bigr => i _; rewrite -mulnDl -eulerS. rewrite big_ord_recr /= euler_small1 // muln0 addn0 // -big_split /=. rewrite expnS Hrec big_distrr /=; apply: eq_bigr => i _ /=. rewrite mulnAC (mulnAC (n.+1 - i)) - mulnDl mulnC (mulnC _ 'Eu(_,_)). rewrite addnS binS (mulnDr (n.+1 - i)) addnA - mulnDl addSn. rewrite subnKC ?(@ltnW i) // -mul_Sm_binm_2 -mulnDl addnBA ? (@ltnW i) //. case (ltnP (k + i) n.+1) => ltnp; first by rewrite (bin_small ltnp) !muln0. by rewrite (subnK ltnp) addnK (mulnC k) mulnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)