proposition: Lemma double_square_square m n: (n ^2).*2 = m ^2 -> n = 0.
proof: Proof. move/eqP. elim: n {-2} n (leqnn n) m; first by move => n; rewrite leqn0 => /eqP. move => k IH n; rewrite leq_eqVlt; case/orP=> [/eqP -> m Hm |Hm]; last first. by apply: IH; rewrite -ltnS. move:(odd_double (k.+1 ^ 2)); rewrite (eqP Hm) odd_sqr => /evenE mv. move: Hm; rewrite mv double_square eqn_double eq_sym => ea. case: (ltnP k (m./2)). by rewrite - leq_sqr - leq_double (eqP ea) leqNgt double_le3. by move => la; move: (ea); rewrite (IH _ la _ ea) (eqn_sqr 0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)