proposition: Lemma fib_sum_square_is_fib_square m n k: 0 < m <= n -> (fib m)^2 + (fib n)^2 = (fib k)^2 -> False.
proof: Proof. move => /andP [la lb] hb. case: (ltnP n k) => cp; last first. move:(fib_monotone cp); rewrite leqNgt => /negP; case. by rewrite -ltn_sqr -(add0n (fib n ^ 2)) -hb ltn_add2r sqrn_gt0 fib_gt0. move:(fib_monotone cp); rewrite -(leq_pmul2l (m:=2)) // => sa. case: (ltngtP 1 n). + move/fib_mon1 => sb; move:(leq_trans sb sa); rewrite leqNgt => /negP. case;rewrite -ltn_sqr !expnMn - hb -[3^2]/(5 + 2^2) mulnDr mulnDl ltn_add2r. apply: (@leq_ltn_trans (4 * fib n ^ 2)). by rewrite leq_pmul2l // leq_sqr fib_monotone. by rewrite ltn_pmul2r // expn_gt0 fib_gt0 // (leq_trans la lb). + by rewrite ltnNge (leq_trans la lb). + move => n1; move: hb; rewrite -n1; move /square_plus1_square => fz. by move: (fib_gt0 la); rewrite fz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)