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