proposition: Lemma square_plus9_square n m: n ^2 + 3^2 = m ^2 -> (n = 0 \/ n = 4).
proof: Proof. case /pythagore_tripleB; [ by case => h _; left | by case | ]. move => [p [q[ha hb hc hd]]] [] [ea eb _]. by move: (f_equal odd eb); rewrite -doubleMr odd_double. rewrite subn_sqr in ea. have /primeP [_ h]: prime 3 by []. have da: (p + q) %| 3 by rewrite ea mulnA /dvdn modnMl. case/orP: (h _ da) => /eqP rv. move: eb hb rv; clear; case: q; first by rewrite !muln0 => ->; left. move => q _ np => /eqP; rewrite addnS eqSS addn_eq0 => /andP [ha hb]. by move: np; rewrite (eqP ha) (eqP hb). move/eqP: ea; rewrite rv mulnA -{1}[3]/(1*3) eqn_pmul2r // eq_sym muln_eq1. move /andP => [r1 pq]. right; move /eqP: rv;rewrite eb (eqP r1) -(subnK (ltnW hb)) (eqP pq). by rewrite -addnA eqSS addnn (eqn_double q 1) => /eqP ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)