proposition: Lemma fib_sum_square_is_fib_square_bis m n k: (fib m)^2 + (fib n)^2 == (fib k)^2 = ((m==0) && (fib n== fib k)) || ((n == 0) && (fib m== fib k)).
proof: Proof. wlog: m n / m <= n. move => H; case/orP:(leq_total m n); first by apply: H. by move => h; rewrite addnC orbC; apply: H. move => mn; case: (posnP m) => mp. by rewrite mp add0n eqn_sqr; case: (posnP n) => np; rewrite ?orbF//?np ?orbb. rewrite (gtn_eqF (leq_trans mp mn)) /=. by apply/eqP /fib_sum_square_is_fib_square; rewrite mn mp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)