proposition: Lemma square_plus1_square_alt m n: n ^2 + 1 = m ^2 -> n = 0.
proof: Proof. move => h. case: (ltnP n m); rewrite -leq_sqr -h addn1 ? ltnn//. rewrite - addn1 sqrnD addnAC addn1 ltnS muln1 - {2} (addn0 (n^2)). by rewrite leq_add2l leqn0 muln_eq0 /= => /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)