proposition: Lemma fib_lt_lucas n: n != 0 -> fib n <= lucas n ?= iff (n==1).
proof: Proof. move => h; rewrite (lucas_fib h); move: h; case:n => // n _. rewrite fibSS /= - addnA addnn eqSS; apply/leqifP. by case:(posnP n) => np; rewrite ? np // ltn_paddr // double_gt0 fib_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)