proposition: Lemma lucas_lucas_fib_square m n k: m <= n -> ((lucas m)^2 + (lucas n^2) == (fib k)^2) = [&& m==2, n==3 & k==5].
proof: Proof. have H x: lucas x = 0 -> False. by move/eqP;rewrite (gtn_eqF(lucas_gt0 x)). move => lemn; apply/eqP/idP; last first. by move =>/and3P [/eqP -> /eqP -> /eqP ->]. move:lemn;rewrite leq_eqVlt; case/orP => lmn. by rewrite (eqP lmn) addnn => /double_square_square => /H. case m0: (m==0). by rewrite (eqP m0) addnC => /square_plus4_square /H. case m1: (m==1). by rewrite (eqP m1) addnC => /square_plus1_square /H. have m2: 2 <= m by move: m0 m1; clear; case:m => [|[]]. have la: 3 <= lucas m by apply: (@lucas_monotone 2). have lb: 4 <= lucas n. by apply: (@lucas_monotone 3); rewrite /=(leq_ltn_trans m2 lmn). have lc: 25 <= lucas m ^ 2 + lucas n ^ 2. move: la; rewrite - leq_sqr => la. move: lb; rewrite - leq_sqr => lb. by rewrite (leq_add la lb). move => h; have ld: 5 <= (fib k) by rewrite -leq_sqr - h. move: h ld; case:k => [|[|[| [| [|]]]]] //; case. case lm2: (m==2). rewrite (eqP lm2) => /eqP. rewrite -[fib 5 ^ 2]/(lucas 2 ^ 2 + lucas 3 ^ 2) eqn_add2l. by rewrite eqn_sqr lucas_injective_bis => ->. have m3: 0 < 3 <= m by rewrite /= ltn_neqAle eq_sym lm2 m2. have: 0 < 4 <= n by rewrite /= (leq_trans _ lmn). move/lucas_monotone ; rewrite -leq_sqr => ha. move:(lucas_monotone m3); rewrite -leq_sqr => hb h. by move:(leq_add hb ha); rewrite h. have Ha a b: a <= a - b + b. case /orP: (leq_total a b) => lab; last by rewrite subnK. move:(lab); rewrite {1} /leq; move => /eqP ->//. move => k. have ->: k.+2.+4 = k+6 by rewrite !addnS addn0. have l05: 0 < 5 by []. have l5_12: 5 <= 12 by []. move:(lucas5S (k.*2+7)); rewrite -(addnA _ 7 5) -[7 + 5]/12 => Lk h _. set x := 5*( (lucas m.*2 + lucas n.*2)). have: (x <= lucas (k.*2+12) + 22) && (lucas (k.*2+12) <= x + 22). move /eqP: h; rewrite -(eqn_pmul2l l05). rewrite !lucas_square mulnA lucas_lucas2 ?leqnn // addnn subnn lucas0. have ->: odd (k + 6) = ~~(odd k.+1) by rewrite oddD addbF/=; case: odd. pose T b x := (if b then subn else addn) x 2. have Ta: forall b x, x <= (T b x) + 2. by rewrite /T;move => b y; case b => //; rewrite -addnA leq_addr. have Tb: forall b x, (T b x) <= x + 2. rewrite /T;move => b y; case b => //; apply: leq_BD. rewrite doubleD if_neg => /eqP ha; apply/andP; split. move:(Tb (odd k.+1) (lucas(k.*2 + 12))); rewrite -(leq_add2r 20) - addnA. move: (leq_add (Ta (odd m) (lucas m.*2)) (Ta (odd n) (lucas n.*2))). rewrite addnACA; rewrite - (leq_pmul2l l05) (mulnDr _ _ 4) ha -/x. apply: leq_trans. apply: (leq_trans(Ta (odd k.+1) (lucas(k.*2 + 12)))). rewrite (addnA _ 20 2) leq_add2r /T -ha /x - (mulnDr 5 _ 4) leq_pmul2l //. rewrite -[4]/(2 +2) addnACA; apply: leq_add; apply: Tb. move /andP => [ha hb]. have le: lucas (k.*2+12) +22 < 5* lucas (k.*2 +9). rewrite Lk (addnS k.*2 8) (addnS k.*2 7). rewrite lucasSS - addnA mulnDr ltn_add2l(mulnDl 3 2) ltn_add2l mul2n. rewrite (ltn_double 11); apply: (@lucas_smonotone 5); rewrite l05 //=. by rewrite -addSnnS -{1} (add0n 6) leq_add2r. have hc: 5 * lucas n.*2 <= x by rewrite /x mulnDr leq_addl. move: (leq_ltn_trans (leq_trans hc ha) le); rewrite ltn_pmul2l //. case: (ltngtP (k.*2 +8) n.*2 ) => hd. by rewrite ltnNge; move/negP; case; apply: lucas_monotone;rewrite addnS hd. have he: x + 22 <= 5 * (lucas n.*2.+1) + 22. move: lmn; rewrite - ltn_double => sa. have hx:= (ltn_predK sa). rewrite leq_add2r /x (leq_pmul2l l05) -{2}hx lucasSS addnC hx leq_add2l. by apply: lucas_monotone; rewrite (ltn_double 0) lt0n m0 - ltnS hx //. have : 22 <3 * lucas (k.*2 +7). apply: ltnW; rewrite (@leq_pmul2l 3 8) => //; apply: (@lucas_smonotone 4). by rewrite /= (addnA _ 2 5) leq_addl. rewrite - (ltn_add2l (5 * lucas n.*2.+1)) => hf. move: (leq_ltn_trans (leq_trans hb he) hf). rewrite Lk ltn_add2r (ltn_pmul2l l05) ltnNge => /negP; case. by apply:lucas_monotone; rewrite - addnS hd. move /eqP: hd; rewrite -(doubleD k 4) eqn_double eq_sym => /eqP hd _. move:ha hb; rewrite /x Lk hd doubleD mulnDr addnC (addnS k.*2 7) - 2!addnA. rewrite !leq_add2l (addnS k.*2 6) (addnS k.*2 5) lucasSS (addnS k.*2 4) lucasSS. rewrite addnAC addnn -(mul2n (lucas _)) mulnDr mulnA => ec ed. set u := lucas (k.*2 + 4).+1 + 3 * lucas (k.*2 + 4). have : 22 < u. apply: (@leq_trans (lucas 5 + 3 * (lucas 4))) => //. by apply: leq_add; rewrite ?(@leq_pmul2l 3)-? addnS //; apply: (lucas_monotone); rewrite /= leq_addl. rewrite -(ltn_add2l (5 * lucas m.*2)) => ef. move:(leq_ltn_trans ed ef); rewrite (mulSnr 5) - addnA ltn_add2r ltn_pmul2l //. move => ww. case: (ltngtP (k.*2 + 4).+2 (m.*2)) => eg. + have: 0 < (k.*2 + 4).+3 <= m.*2 by rewrite eg. move/lucas_monotone; rewrite -(leq_pmul2l l05) => sa. move:(leq_trans sa ec); rewrite lucasSS mulnDr (mulSnr 5) - 2!addnA. rewrite addnC leq_add2l lucasSS mulnDr (addnC _ 22) (mulSn 4) - addnA. rewrite leq_add2l (mulnDl 2 3) addnA leq_add2r. have: 0 < 4 <= (k.*2 + 4).+1 by rewrite /= -addSn leq_addl. move/lucas_monotone;rewrite -(@leq_pmul2l 4) // => sb sc. have sd: 22 < 4* lucas 4 by []. move: (leq_trans (leq_ltn_trans sc sd) sb). rewrite ltnNge; move/negP; case; apply: leq_addr. + move: ww; rewrite ltnNge => /negP; case; apply: lucas_monotone. by rewrite - (ltnS m.*2) eg double_gt0 lt0n m0. + move:ec; rewrite - eg lucasSS mulnDr (mulSnr 5) - 2!addnA leq_add2l. rewrite (addnC _ 22) addnA (mulnDl 2 3) leq_add2r addnS lucasSS mul2n - addnn. rewrite - addnA leq_add2l addnS lucasSS leq_add2l. move: eg; rewrite -!addnS -(doubleD k 3) =>/eqP; rewrite eqn_double =>/eqP ha. have L1: lucas 1 = 1 by rewrite lucas1. have L2: lucas 2 = 3 by []. have L3: lucas 3 = 4 by rewrite lucasSS. have L4: lucas 4 = 7 by rewrite lucasSS L3 L2. have L5: lucas 5 = 11 by rewrite lucasSS L4 L3. have L6: lucas 6 = 18 by rewrite lucasSS L5 L4. have L7: lucas 7 = 29 by rewrite lucasSS L6 L5. have F5: fib 5 = 5 by []. have F6: fib 6 = 8 by rewrite fibSS F5. have F7: fib 7 = 13 by rewrite fibSS F6 F5. have F8: fib 8 = 21 by rewrite fibSS F6 F7. move: h; rewrite hd - ha; case k => [|[ | [| k']]]; rewrite ? L3 ? L4 ? L5 ? L6 ? F5 ? F6 ? F7 ? F8 //. have: 0 < 8 <= ((k'.+3).*2 + 2) by rewrite /= addn2 !doubleS //. move/lucas_monotone => sa _ sb. by move: (leq_trans sa sb); rewrite lucasSS L7 L6. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)