proposition: Lemma square_plus4_square m n: n ^2 + 4 = m ^2 -> n = 0.
proof: Proof. move => h; move:(subn_sqr m n); rewrite - h addKn. case: (ltnP m n); first by rewrite -ltn_sqr - (addn0 (n^2)) -h ltn_add2l. move => ha; rewrite -{2} (subnK ha)- addnA addnn. rewrite -(odd_double_half (m-n)); case: odd. by move => eqA; move:(f_equal odd eqA); rewrite oddM !oddD !odd_double. move/esym; move/eqP; rewrite -[4]/(1.*2.*2) add0n -doubleD -doubleMr. by rewrite -doubleMl 2!eqn_double muln_eq1 => /andP[/eqP -> /eqP]; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)