proposition: Lemma lucas_fib n: n != 0 -> lucas n = fib n.+1 + fib n.-1.
proof: Proof. elim: n {-2}n (leqnn n)=> [ [] // |n IH n1]. rewrite leq_eqVlt; case/orP=> [|Hn1]; last by apply: IH; rewrite -ltnS. move/eqP->; case: n IH=> [|[|n] IH _] //. by rewrite lucasSS !IH // addnCA -addnA -fibSS addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)