proposition: Lemma euler_small n p: 'Eu(n, n+p) = 0.
proof: Proof. move: p; elim: n => [p // | n Hrec p]. by rewrite addSn eulerS -addnS 2!Hrec 2!muln0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)