proposition: Lemma lucas_lt_fib n: n != 0 -> lucas n <= fib n.+2 ?= iff (n==2).
proof: Proof. move => h; rewrite (lucas_fib h) fibSS; apply/leqifP. move:h; case:n =>[ | [| [| n]]] //= _ ;rewrite ltn_add2l fib_smonotone //=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)