fact: Fixpoint euler_rec n m := match n, m with | n'.+1, m'.+1 => m.+1 *euler_rec n' m + (n'-m') * euler_rec n' m' | 0, _ => 0 | _.+1, 0 => 1 end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)