proposition: Lemma lucas_square_bound n: 3 <= n -> fib n.*2.+1 < (lucas n)^2 < fib n.*2.+2.
proof: Proof. rewrite lucas_square. have ha k: 2 < fib k .+1.+4 by rewrite (fib_smonotone_bis (a:=1)) //. case: (odd_dichot n) => -> /=; rewrite odd_double /=. case: (n./2) => //k _; rewrite !doubleS lucas_fib //;have hb:= (ha k.*2.*2). rewrite -(subnK (ltnW hb)) addnA addnK ltn_paddr ? subn_gt0 //. rewrite (fibSS (k.*2).*2.+4.+2) ltn_add2l (fibSS (k.*2).*2.+4). by apply /(leq_ltn_trans (leq_subr 2 _)) /ltn_paddr /fib_gt0. case:(n./2) => [// | [// | m _]]. rewrite !doubleS lucas_fib //; set k := (m.*2).*2.+4.+2. by rewrite - addnA {1} addn2 ltn_paddr //= (fibSS k.+2) (fibSS k) !ltn_add2l ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)