proposition: Lemma square_plus4_square_alt2 m n: n ^2 + 4 = m ^2 -> n = 0.
proof: Proof. rewrite -[4]/(2^2) => h; apply/eqP. case:(Fermat2_bound2 h). rewrite muln2 addn2 double_eq0 2!leq_eqVlt 2!ltnS. rewrite addnC in h; move/leqifP:(Fermat2_bound h) => /= lnm. rewrite leqNgt lnm /=; case/orP; first by move->. rewrite orbF eqSS => /eqP k; move:(congr1 odd h). by rewrite k oddD !odd_sqr/=; case: odd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)