proposition: Lemma Fermat4_alt x y z (pa:= fun x => exists y, x= y^2 \/ x = (y^2).*2) (pb := fun x y z => [\/ pa x /\ pa y, pa y /\ pa z | pa z /\ pa x]): x^2 + y ^2 = z ^2 -> coprime x y -> pb x y z -> (x == 0) || (y == 0).
proof: Proof. elim: z {-2} z (leqnn z) x y. move => z; rewrite leqn0 => /eqP -> x y /eqP; rewrite addn_eq0 expn_eq0 //. by rewrite andbT; move/andP => [->]. move => K Hrec z zB x y ha hb hc. wlog: x y ha hb hc /(odd y). move => H; move:(pythagore_mod4 hb ha); case oy: (odd y). by move => _; apply: H. rewrite coprime_sym in hb; rewrite addnC in ha; rewrite negb_eqb addbF orbC. apply: H => //; case: hc => [][qa qb]. - by constructor 1. - by constructor 3. - by constructor 2. move => oy; case: (pythagore_tripleB ha). by move => [->]. by move => [->]; rewrite orbT. move => [p [q []]]; rewrite (eqP hb) !mul1n => _ lqp cp2 opq. case => [][yv xv zv]; first by move: oy; rewrite xv odd_double. have oz: odd z by rewrite -odd_sqr - ha oddD !odd_sqr oy xv odd_double. have paw w: pa w -> odd w ->exists y', w = y'^2. move => [t]; case => ->; [ by exists t | by rewrite odd_double]. have lb: (q ^ 2) <= (p ^ 2) by rewrite leq_sqr (ltnW lqp). have la: (q ^ 2) ^ 2 <= (p ^ 2) ^ 2 by rewrite leq_sqr. have zz: z = 0 -> (x == 0) || (y == 0). by move => h; move /eqP:ha; rewrite h addn_eq0 !expn_eq0 !andbT => /andP[->]. case (posnP q) => qp; first by rewrite xv qp !muln0. case (posnP p) => pp; first by rewrite xv pp. have pax: pa x -> pa p /\ pa q. rewrite xv; move: opq cp2; rewrite negb_eqb; clear;wlog: p q /odd p. move => H; case op: (odd p) => ww; first by apply:H => //; rewrite op. rewrite coprime_sym mulnC=> sa sb. simpl in ww; have opq: odd q (+) odd p by rewrite ww op. by case: (H q p ww opq sa sb). case: (posnP p) => pp; first by rewrite pp. move => op; rewrite op /= => oq cpq [t]; case. rewrite - muln2 -mulnA (mulnC q) => eqa. have cp': coprime p (2 * q) by rewrite /coprime Gauss_gcdr // coprimen2. case: (factor_square pp cp' eqa); set u:= _ %/ _; set v := _ %/ _. move => -> hb hc. move:(f_equal odd (esym hb)); rewrite odd_sqr mul2n odd_double => ov. split; first by exists u; left. move /eqP: hb; rewrite (evenE ov) - mul2n expnMn - (mulnA 2 2) !mul2n => h. by exists (v./2); right; apply/eqP; rewrite -eqn_double h. move/eqP; rewrite eqn_double => /eqP eqa. case: (factor_square pp cpq eqa); set u := _ %/ _; set v := _ %/ _. move => -> -> cp;split; [ by exists u; left | by exists v; left]. have lpk: p^2 <= K. by rewrite -ltnS; apply: leq_trans zB; rewrite zv ltn_paddr // sqrn_gt0. have lpk1: p <= K. by apply: leq_trans lpk; rewrite -{1}(expn1 p) leq_pexp2l. case: hc => [] [he hf]. + move: (paw _ hf oy) => [y' y'v]. move: (pax he)=> [sa sb]. have eq2: q ^ 2 + y' ^ 2 = p ^ 2 by rewrite -y'v yv subnKC. have cp3: coprime q y'. by rewrite -coprime_sqr -coprimeDl eq2 coprime_sqr coprime_sym. have rc: pb q y' p by constructor 3. move: (Hrec p lpk1 q y' eq2 cp3 rc); rewrite (gtn_eqF qp) /= y'v => /eqP. by move => ->; rewrite orbT. + move: (paw _ he oy) => [y' ysv]; move: (paw _ hf oz) => [z' zsv]. have ra:(y' * z') ^ 2 + (q ^ 2) ^ 2 = (p ^ 2) ^ 2. by rewrite expnMn - ysv - zsv yv zv - subn_sqr subnK. have rb:coprime (y' * z') (q ^ 2). by rewrite -coprime_sqr coprime_sym - coprimeDr ra !coprime_sqr coprime_sym. have rc:pb (y' * z') (q ^ 2) (p ^ 2). constructor 2; split; [ by exists q; left | by exists p; left]. move: (Hrec (p^2) lpk (y'*z') (q^2) ra rb rc). rewrite expn_eq0 (gtn_eqF qp) muln_eq0 orbF; case/orP => /eqP hw. by rewrite ysv hw orbT. by apply:zz; rewrite zsv hw. + move: (paw _ he oz) => [z' z'v]. move: (pax hf)=> [sa sb]. have eq2: p ^ 2 + q ^ 2 = z' ^ 2 by rewrite - z'v zv. have pbb: pb p q z' by constructor 1. have lt1: z' <= K. move: (qp)(pp); rewrite - sqrn_gt0 - (sqrn_gt0 p) => l1 l2. move:(leq_add l2 l1) zB; rewrite - zv z'v; clear; case z' => //; case=> //. move => n nb nc; rewrite - ltnS; apply: leq_trans nc. by rewrite - mulnn; apply:ltn_Pmull. by move: (Hrec z' lt1 p q eq2 cp2 pbb); rewrite (gtn_eqF qp) (gtn_eqF pp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)