proposition: Lemma lucas_fib: forall n, n != 0 -> lucas n = fib n.+1 + fib n.-1.
proof: Proof. move=> n; elim: n {-2}n (leqnn n)=> [[] // _ |n IH]. move=> n1; rewrite leq_eqVlt; case/orP=> [|Hn1]; last first. by apply: IH; rewrite -ltnS. move/eqP->; case: n IH=> [|[|n] IH _] //. by rewrite lucasSS !IH // addnCA -addnA -fibSS addnC. Qed.
imports: mathcomp(all_ssreflect all_algebra)