fact: Fixpoint lucas_rec n := if n is n1.+1 then if n1 is n2.+1 then lucas_rec n1 + lucas_rec n2 else 1 else 2.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)