proposition: Lemma fib_lt_exp n: 2 <= n -> fib n.+2 < 2^n.
proof: Proof. move/ subnK => <-. pose p k := fib (k + 2).+2 < 2 ^ (k + 2). suff: p (n-2) /\ p (n-2).+1 by case. elim: {n} (n -2) => // k [ha hb]; split => //. move:(leq_add hb (ltnW ha));rewrite /p !addSn - fibSS => sa. apply: (leq_trans sa). by rewrite (expnS _ _.+1) mul2n -addnn leq_add2l leq_exp2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)