proposition: Lemma eulern3 n: 'Eu(n,3) + 3^n * (n.+1) + 'C(n.+1, 3) = 4 ^n + 2^n * 'C(n.+1, 2).
proof: Proof. elim:n => [// | n Hrec]; rewrite eulerS (binS n.+1 2) (addnC 'C(n.+1, 3)). rewrite addnA - (addnA (4 * _)) - (addnA (4 * _)). apply /eqP; rewrite - (eqn_add2r (4 * 3 ^ n * n.+1 + 3 * 'C(n.+1, 3))). rewrite - addnA (addnCA 'C(n.+1, 3)) - addnA - mulSn - mulnA - mulnDr. rewrite (addnC _ (4 * _)) addnA - mulnDr (addnA ('Eu( _,_))) Hrec {Hrec}. rewrite mulnDr - expnS - mul_Sm_binm_2 mulnA - (mulnA 2 2) -expnS -mulnA. rewrite mul2n -addnn (addnA (4 ^ n.+1)) (binS n.+1 1) mulnDr - 5!addnA. apply /eqP; congr (_ + (_ + _)); case:n => // n; case :n => // n. rewrite 4! subSS 2!subn0 expnS (mulnC 2) -mulnA (mulnC 2) bin2' -{1}(bin1 n.+3). rewrite - {2} (addn2 n) mulnDl mulnDr mulnCA addnAC addnA - mulnDr. rewrite (addnC _ 'Eu(n.+2, 2)) eulern2 addnC mulnA; congr (_ + _). rewrite mulnDr addnAC addnA (expnS _ n.+2) mulnAC - mulnDl - addnA. by rewrite - mulSn mulnS addnA addn3 - mulSn mulnAC mulnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)