proposition: Lemma lucas_fib_lucas_square m n k: ((fib m)^2 + (lucas n^2) == (fib k)^2) = ((m==0) && (fib k == lucas n)) || [&& k ==5, m==4 & n==3].
proof: Proof. case :(posnP m) => mz; first by rewrite mz eqn_sqr eq_sym /= !andbF orbF. have fmp:=(fib_gt0 mz). have fm: ~(fib m = 0) by move => h; move: fmp; rewrite h. case:n => [|[|[| [|n]]]]. + by rewrite /= !andbF; apply/negP => /eqP /square_plus4_square. + by rewrite /= !andbF; apply/negP => /eqP /square_plus1_square. + rewrite -[lucas 2]/(fib 4). by rewrite (fib_sum_square_is_fib_square_bis) (gtn_eqF mz) !andbF. rewrite -[lucas 3 ^ 2]/(4 ^2) square_plus16_square (gtn_eqF fmp) /=. + by rewrite (fib_eq m 4) (fib_eq k 5) /= !andbF !orbF andbT andbC. + rewrite !andbF /=; apply/negP => /eqP. have ln : ~(lucas n.+4 = 0) by move => h; move: (lucas_gt0 n.+4);rewrite h. case: (ltngtP (fib m) (lucas n.+4)); last first. by move => ->; rewrite addnn; move/double_square_square. move => sa sb. case: (ltnP m k) => ha. move: (mz); rewrite leq_eqVlt; case/orP => m2. by move: sb; rewrite addnC - (eqP m2); move /square_plus1_square. move:(fib_mon1 m2); rewrite - leq_sqr !expnMn => h. move: (fib_monotone ha); rewrite - leq_sqr => sc. have: (lucas n.+4) ^2 < (fib m)^2 by rewrite ltn_sqr sa. rewrite -(ltn_add2l (fib m ^ 2)) sb addnn - mul2n => sd. move: (leq_ltn_trans sc sd); rewrite -(@ltn_pmul2l 4) // mulnA => hc. by move:(leq_ltn_trans h hc); rewrite (ltn_pmul2r) // sqrn_gt0. move: (fib_monotone ha); rewrite -leq_sqr - sb leqNgt => /negP; case. by rewrite -{1} (addn0 (fib m ^ 2)) ltn_add2l sqrn_gt0 lucas_gt0. move => sa sb; case: (ltngtP k (n.+4.+2))=> kn4. + have hh: lucas n.+4 < fib k. by rewrite -ltn_sqr -(add0n (lucas n.+4 ^ 2)) - sb ltn_add2r sqrn_gt0. rewrite ltnS in kn4; move: (leq_trans hh (fib_monotone kn4)). by rewrite lucas_fib //= -{2} (addn0 (fib n.+4.+1)) ltn_add2l ltn0. + move:(fib_monotone kn4); rewrite fib3S -leq_sqr. move: sa; rewrite -ltn_sqr -(ltn_add2r (lucas n.+4 ^ 2)) sb addnn => sc sd. move: (leq_ltn_trans sd sc); rewrite ltnNge => /negP; case. rewrite sqrnD lucas_fib //= sqrnD 2!doubleD - 2!addnA -(muln2 (fib n.+4.+1)). have: (fib n.+4.+1 ^ 2).*2 + (fib n.+3 ^ 2).*2 <= (fib n.+4.+1 * 2) ^ 2. rewrite expnMn - doubleD (mulnA _ 2 2) muln2 muln2 leq_double - addnn. by rewrite leq_add2l leq_sqr fib_monotone // ltnS; apply: ltnW; apply: ltnW. rewrite -(@leq_add2r (fib n.+4 ^ 2 + 2 * (fib n.+4.+1 * 2 * fib n.+4))) => ww. apply:leq_trans ww; rewrite - addnA leq_add2l leq_add2l (mulnC _ 2) -mul2n. apply: (@leq_trans (2 * (2 * (fib n.+4.+1 * fib n.+4)))). by rewrite !leq_pmul2l //? fib_gt0 // fib_monotone. by rewrite - mulnA leq_addl. move /eqP: sb; rewrite kn4 lucas_fib //= fib3S (fib3S n.+3) addnAC - addnA. rewrite -fibSS - !mul2n 2!sqrnD 2!expnMn mulnAC addnA eqn_add2r addnA. rewrite (mulSnr 3) (mulSn 3) - (addnA (fib n.+4 ^ 2)) addnC eqn_add2l. rewrite addnA eqn_add2r => sx. have sc: 3 * (fib n.+3)^2 < 2 *(fib n.+4)^2. have ww: 1 < n.+3 by []. move:(fib_mon1 ww); rewrite - (@leq_pmul2r (fib n.+3)) ? fib_gt0 // => h. rewrite - mulnn - mulnn 2!mulnA; apply: (leq_ltn_trans h). by rewrite (ltn_pmul2l) // ?fib_smonotone //= muln_gt0 fib_gt0. have sb: 3 * fib n.+4 ^ 2 < (fib n.+4.+2)^2. rewrite (fibSS (n.+4)) (fibSS (n.+3)) addnAC addnn sqrnD - addnA. rewrite -mul2n expnMn (mulSnr 3) -addnA -[X in X < _] (addn0) ltn_add2l. by rewrite addn_gt0 sqrn_gt0 fib_gt0. case: (ltngtP m n.+4.+1). + rewrite ltnS; move/fib_monotone; rewrite leqNgt - ltn_sqr. by rewrite -(ltn_add2r (2 * fib n.+4 ^ 2)) - mulSn - (eqP sx) ltn_add2l sc. + move/fib_monotone; rewrite -leq_sqr => sd. by move:(leq_trans sb sd); rewrite - (eqP sx) ltnNge leq_addr. + move => eq1. move: sx; rewrite (fib_square_succ n.+2) addnC mulnDr eqn_add2l eq1. rewrite -mulnn mulnA eqn_pmul2r ? fib_gt0 // fib4S - {2}(addn0 (3 *_)). rewrite eqn_add2l double_eq0 fib_eq0 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)