proposition: Fact square_plus16_square_alt n m: (n ^2 + 4^2 = m ^2) -> n = 0 \/ n = 3.
proof: Proof. case /pythagore_tripleB; [ by case => h _; left | by case | ]. have H1 a b: 2 == a * b -> (a==1) || (a == 2). by case: a => [|[|[| a]]] => //; rewrite mulnC;case: b. have H a b: odd b -> 2 == a * b -> (a == 2). move => ob h; case/orP: (H1 _ _ h);last by move => ->. by move => /eqP a1; move:(f_equal odd (eqP h)); rewrite a1 mul1n ob. move => [p [q[ha hb hc hd]]]; case; case => ea eb ec. move/eqP: eb; rewrite -{1}[4]/(2.*2) -doubleMr eqn_double => ed. case opq: (odd (p * q)). move: opq hd; rewrite oddM; case: odd; case: odd => //=. move: ed; rewrite -{1} [2]/(1.*2) (evenE opq) -doubleMr eqn_double eq_sym. rewrite muln_eq1 -(eqn_double _./2) -(evenE opq) => /andP [g1 g2]. rewrite eq_sym in g2;case/orP: (H1 _ _ g2) => /eqP pv; rewrite pv in g2. by rewrite mul1n in g2; move: hb; rewrite -(eqP g2) pv. by right;move: g2; rewrite ea (eqP g1) mul1n pv mul2n eqn_double => /eqP <-. have hb':= (ltnW hb). have od: odd (p^2 - q^2). by rewrite oddB ?leq_sqr // !odd_sqr -negb_eqb. have g4: gcdn n 4 = 4. move: (f_equal odd ea); rewrite oddM od /= andbT => /esym neg. move: ea;rewrite (evenE neg) -[4]/(2.*2) -doubleMl => /eqP. by rewrite eqn_double => h; rewrite (eqP (H _ _ od h)). move /eqP:ea; rewrite g4 -{1} (muln1 4) eqn_pmul2l // eb => /eqP h. have: q^2 + 1 = p ^2 by rewrite {2} h subnKC // leq_sqr. by move/ square_plus1_square => ->; left; rewrite !muln0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)