proposition: Lemma lucas_ge2 n: n !=1 -> lucas n = (lucas n).-2.+2.
proof: Proof. case:n => //; case => // n _. by rewrite -(subnK (lucas_gen n.+2)) 2! addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)