proposition: Lemma square_plus16_square n m: (n ^2 + 4^2 == m ^2) = (n==0) && (m==4)||(n==3)&&(m==5).
proof: Proof. apply/idP/orP; last by case => /andP [/eqP -> /eqP ->] //. case:(ltnP n m); last first. move => cap; have /gtn_eqF -> //: m^2 < n ^ 2 + 4^2. by apply: (@leq_ltn_trans (n^2)); rewrite ? leq_sqr // -addSnnS leq_addr. move => lnm /eqP h; move: lnm; rewrite leq_eqVlt; case/orP => lmn. by move:(congr1 odd h); rewrite -(eqP lmn) oddD !odd_sqr /=; case: odd. move:lmn; rewrite -(leq_sqr) - addn2 -h sqrnD - addnA leq_add2l. rewrite - [4 ^ 2]/( 2 ^ 2 + 4 * 3) leq_add2l (mulnC n) mulnA leq_pmul2l //. rewrite leq_eqVlt; case/orP => n3; [right | left]. by move/eqP: h; rewrite (eqP n3) (eqn_sqr 5) eq_sym. case: (Fermat2_bound h); rewrite leq_eqVlt eq_sym -leq_sqr -h. by rewrite -[5^2]/(3^2+4^2) leq_add2r leq_sqr -ltnS ltnNge n3 orbF => -> <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)