proposition: Lemma fib_square_bound n: 2 <= n -> fib n.*2 < (fib n.+1)^2 < fib n.*2.+1.
proof: Proof. move => ha;rewrite fib_doubleS -{2}(addn0 ((fib n.+1)^2)) ltn_add2l sqrn_gt0. rewrite (fib_gt0 (ltnW ha)) andbT. rewrite -(ltn_add2l (fib n.+1 * (fib n).*2)) -mulnn -mulnDr. rewrite -fib_double doubleS fibSS ltn_add2r fib_doubleS -muln2 mulnA mulnC. have hb: fib n < fib n.+1 by rewrite fib_smonotone // ha leqnn. by move/leqifP:(nat_Cauchy (fib n.+1) (fib n)); rewrite (gtn_eqF hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)