proposition: Lemma euler_sub n m: m <=n -> 'Eu(n.+1,m) = 'Eu(n.+1, n-m).
proof: Proof. move: m; elim: n; first by case. move => n Hrec m; rewrite leq_eqVlt; move/orP; case. by move /eqP => ->; rewrite euler_nn subnn eulern0. rewrite ltnS; case: m; first by rewrite subn0 euler_nn eulern0. move => m le1; rewrite (subSn le1) eulerS (eulerS n.+1) (subnSK le1). rewrite addnC (subSn (ltnW le1)) (Hrec _ (ltnW le1)) (Hrec _ le1). by rewrite (subSn (leq_subr _ _)) (subnBA _ le1) addKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)