proposition: Lemma square_plus2_square m n: n ^2 + 2 = m ^2 -> False.
proof: Proof. move => eq1. case: (ltnP n m);rewrite -leq_sqr -eq1; last by rewrite leqNgt ltn_paddr. rewrite -addn1 sqrnD -addnA leq_add2l muln1 mul2n add1n (ltn_double n 1). by move: eq1; case: n => //=; rewrite add0n; move/(@double_square_square m 1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)