proposition: Lemma euler_sum n : \sum_(i<n.+1) 'Eu(n.+1,i) = (n.+1)`!.
proof: Proof. elim:n => [|n IHn]; first by rewrite big_ord_recl big_ord0 addn0. rewrite big_ord_recl eulern0. transitivity (1 + (\sum_(i < n.+1) (i.+2) * 'Eu(n.+1, lift ord0 i) + (\sum_(i < n.+1) (n.+1 -i) * 'Eu(n.+1, i)))). congr (_ + _); rewrite -big_split /=; apply: eq_bigr => i _; apply: eulerS. rewrite big_ord_recr big_ord_recl /= euler_small1 // muln0 addn0 muln1 subn0. rewrite (addnCA _ n.+1) addnA add1n - big_split /= factS -IHn. rewrite big_ord_recl eulern0 mulnDr muln1 big_distrr /=; congr (_ + _). apply: eq_bigr; move => [i lin] _; rewrite -mulnDl /= (subSn lin). by rewrite (subnSK lin) - add2n - addnA (addnC i) add2n subnK ? (ltnW lin). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)