proposition: Fact square_plus4_square_alt m n: n ^2 + 2^2 = m ^2 -> n = 0.
proof: Proof. have: prime 2 by []; move/primeP => [_ dvd2]. case /pythagore_tripleB; [ by case => h | by case | ]. move => [p [q [ha hb hc hd]]]; case; case => ea eb ec. move/eqP: eb;rewrite {2} ea -doubleMr (eqn_double 1) eq_sym !muln_eq1. by move => /and3P [ /eqP -> /eqP -> /eqP -> ]. rewrite subn_sqr in ea. have he: (p + q) %| 2 by rewrite ea mulnA /dvdn modnMl. case/orP: (dvd2 _ he) => /eqP. move: eb; clear; case: q; first by rewrite !muln0. move => q av /eqP; rewrite addnS eqSS addn_eq0 => /andP [ha hb]. by rewrite av (eqP ha) muln0. by move/(f_equal odd); rewrite oddD -negb_eqb hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)