proposition: Lemma square_plus1_square m n: n ^2 + 1 = m ^2 -> n = 0.
proof: Proof. rewrite -{2}[1]/(1^2) => h; apply/eqP. case:(Fermat2_bound2 h);rewrite muln1 addn1 leq_eqVlt ltnS; case: eqP => //= _. by rewrite addnC in h; case:(Fermat2_bound h); rewrite eqn_leq => -> /= ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)