proposition: Lemma euler_sum_aux n p: \sum_(i<n.+1) 'Eu(n.+1,i) * 'C(i,p) = 'Sj(n.+1, n.+1 - p).
proof: Proof. move:p; elim: n. move => p; rewrite big_ord_recl big_ord0 /=; case p => //. move => n Hrec p. case (ltnP n.+1 p) => ltnp. move : (ltnp); rewrite - subn_eq0 => /eqP ->; rewrite nbsurjn0 big1 //. move => [i lin] _; rewrite bin_small ?muln0 //. apply: (leq_trans lin ltnp). move: ltnp; case: p. move => _; rewrite subn0 nbsurj_nn - euler_sum; apply: eq_bigr. by move => i _; rewrite bin0 muln1. move => p ltnp; rewrite (subSn ltnp) nbsurjS - Hrec subSS - {2} subSn //. rewrite - Hrec - big_split big_distrr /= big_ord_recl add0n. transitivity (\sum_(i < n.+1) (i.+2) * 'Eu(n.+1, i.+1) * 'C(i.+1, p.+1) + \sum_(i < n.+1) (n.+1-i) * 'Eu(n.+1, i) * 'C(i.+1, p.+1)). rewrite - big_split /=; apply: eq_bigr => i _. by rewrite - mulnDl - eulerS. have ->: \sum_(i < n.+1) i.+2 * 'Eu(n.+1, i.+1) * 'C(i.+1, p.+1) = \sum_(i < n.+1) i.+1 * 'Eu(n.+1, i) * 'C(i, p.+1). rewrite big_ord_recr /= euler_small1 // muln0 addn0. by symmetry; rewrite big_ord_recl /= add0n. rewrite -big_split /=; apply: eq_bigr; move => [i lein] _ /=. set x := 'Eu(n.+1, i). rewrite 2! (mulnC _ x) -2! mulnA - 2! mulnDr (mulnCA _ x); congr (_ * _). rewrite binS mulnDr addnA -mulnDl addSn subnKC ? (ltnW lein) //. case (ltnP i p) => ltip. by rewrite bin_small ? leqW // bin_small // 3!muln0. rewrite mulnDr addnC {1} (_: (n - p).+1 = (n.+1 - i) + (i - p)). by rewrite mulnDl mul_Sm_binm_2 -addnA -mulnDl addSn addnS subnKC. by rewrite ltnS in lein; rewrite subSn // addSn - {1} (subnK lein) addnBA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)