proposition: Lemma lucas_sum_square_is_lucas_square m n k: m <= n -> (lucas m)^2 + (lucas n)^2 = (lucas k)^2 -> False.
proof: Proof. move => la hb. case kz: (k==0). case n1: (n == 1). by move:la hb; rewrite (eqP kz)(eqP n1); case:m => [|[|]]. have lb: 1 <= lucas m ^ 2 by rewrite (ltn_sqr 0) lucas_gt0. have lc: 4 <= lucas n ^ 2. move:n1;rewrite (leq_sqr 2); case: (n) => [|[|u _]] //. by apply: ltnW;apply: (@lucas_monotone 2). by move: (leq_add lb lc); rewrite hb (eqP kz). case: (ltnP n k) => cp; last first. have: 0 < k <= n by rewrite lt0n kz cp. move/lucas_monotone; rewrite leqNgt => /negP; case. by rewrite -ltn_sqr -(add0n (lucas n ^ 2)) -hb ltn_add2r sqrn_gt0 lucas_gt0. have HH x: 8< x.+3 ^ 2 by rewrite (leq_sqr 3 x.+3) //. have Ha x : x ^2 = 5 -> False. by case: x => [|[|[|x h]]] //; move: (HH x); rewrite h. have Hb x : x ^2 = 8 -> False. by case: x => [|[|[|x h]]] //; move: (HH x); rewrite h. case: (ltnP 2 n); last first. rewrite leq_eqVlt ltnS leq_eqVlt ltnS leqn0; case/or3P => n1. + move: la hb; rewrite (eqP n1);rewrite leq_eqVlt ltnS leq_eqVlt ltnS leqn0. case/or3P => m1. - by rewrite (eqP m1) addnn => /double_square_square. - by rewrite (eqP m1) addnC => /square_plus1_square. - rewrite (eqP m1) -[LHS]/13; case: (k) => [|[|[|x h]]] //. suff // : 0 < 3<=x.+3 by move/lucas_monotone; rewrite -leq_sqr -h. + move: hb; rewrite (eqP n1); move/square_plus1_square => lz. by move:(lucas_gt0 m); rewrite lz. + by move: la hb; rewrite (eqP n1) leqn0 => /eqP -> /esym /Hb. move /lucas_mon1 => sb. have: 0 < n.+1 <= k by rewrite cp. move/lucas_monotone; rewrite -(leq_pmul2l (m:=2)) // => sa. move:(leq_trans sb sa); rewrite leqNgt => /negP; case. rewrite -ltn_sqr !expnMn - hb -[3^2]/(5 + 2^2) mulnDr mulnDl ltn_add2r. case mz: (m==0). move: hb; rewrite (eqP mz); case:(n) =>[| [| n1]]. + by move/esym/Hb. + by move/esym/Ha. + move => _; apply: (@leq_trans 45) => //;rewrite (@leq_pmul2l 5 9) //. by rewrite (leq_sqr 3); apply:(@lucas_monotone 2). apply: (@leq_ltn_trans (4 * lucas n ^ 2)). by rewrite leq_pmul2l // leq_sqr lucas_monotone // la lt0n mz. by rewrite ltn_pmul2r // expn_gt0 lucas_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)