proposition: Lemma eulern1 n: 'Eu(n,1) + 'C(n.+1, 1) = 2 ^ n.
proof: Proof. elim:n => [// | n Hrec]; rewrite eulerS expnS - Hrec mulnDr - addnA {Hrec}. by case: n => // n; rewrite eulern0 2!bin1 subn0 muln1 - addSnnS addnn -mul2n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)