proposition: Lemma Fermat4 x y z : x^2 + y^4 = z^4 -> (x == 0) || (y == 0).
proof: Proof. case: (posnP x) => xp //. case: (posnP y) => yp //=. case:(gcd_aux z yp); set a := _ %/ _; set b := _ %/ _; set r := gcdn y z. move => sa sb cp eqa. move: (subn_sqr (z^2) (y^2)); rewrite -!expnM - eqa addnK sa sb. rewrite !expnMn - mulnDl -mulnBl mulnACA mulnn => eqb. have rp: 0 < r by rewrite gcdn_gt0 yp. have: (r^2)^2 %| x ^2 by rewrite eqb /dvdn modnMl. rewrite dvdn_pexp2r // => /dvdnP [c xv]. move /eqP: eqb; rewrite xv expnMn eqn_pmul2r ?expn_gt0 ? rp// => eqc. have ap: 0 < a by move: yp; rewrite sa muln_gt0 rp andbT. have: a < b. rewrite -ltn_sqr ltnNge /leq; apply/eqP => h. by move: xp; rewrite -ltn_sqr xv expnMn (eqP eqc) h. move: (leqnn b) cp eqc ap; clear; elim: b {-2} b a c. by move => b a c; rewrite leqn0 => /eqP ->; rewrite ltn0. move => K IH b a c ns cab eqa ap lab. have ha: a ^ 2 <= b ^ 2 by rewrite leq_sqr (ltnW lab). have eqd: c^2 + (a^2)^2 = (b^2)^2. by rewrite (eqP eqa) - subn_sqr subnK // leq_sqr. case: (posnP c) => cp; first by move/eqP:eqd;rewrite cp 2!eqn_sqr (ltn_eqF lab). move: (cab). rewrite - 2!coprime_sqr -eqd addnC coprimeDl coprime_sym coprime_sqr => cac. case oa: (odd a). case: (pythagore_tripleB eqd). + by case => /eqP; rewrite (gtn_eqF cp). + by case => /eqP; rewrite expn_eq0 andbT (gtn_eqF ap). + move => [p [q []]]; rewrite (eqP cac) ! mul1n => _ sb sc sd [][qa qb qc]. by move: (f_equal odd qb); rewrite odd_sqr odd_double oa. case:(posnP q) => qp; first by move: cp; rewrite qb qp !muln0. have lpk: p <= K. rewrite -ltnS; apply: leq_trans ns. by rewrite -ltn_sqr qc ltn_paddr // expn_gt0 qp. by apply: (IH p q (a*b)) => //; rewrite 1? coprime_sym // -qa -qc expnMn. case ob: (odd b); last first. move: cab;rewrite (evenE oa) (evenE ob) -!muln2. by rewrite /coprime -muln_gcdl muln_eq1 andbF. have cp2: coprime (b ^ 2 - a ^ 2) (b ^ 2 + a ^ 2). have cp1:coprime (b ^ 2 + a ^ 2) 2. by rewrite coprimen2 oddD !odd_sqr oa addbF. rewrite /coprime gcdnC -gcdnDl -addnA subnKC // addnn -muln2 Gauss_gcdl //. by rewrite gcdnC gcdnDl gcdnC -/(coprime _ _) coprime_sqr. move /eqP: (eqa); move/esym => eqa'. case: (posnP (b ^ 2 - a ^ 2)) => dp. by move: cp; rewrite -sqrn_gt0 - eqa' dp. case: (factor_square dp cp2 eqa'); set t := _ %/ _; set s := _ %/ _. move => t2 s2 cst. have os: odd s by rewrite -odd_sqr -s2 oddD !odd_sqr oa ob. have ot: odd t by rewrite -odd_sqr -t2 oddB // !odd_sqr oa ob. move: (oddE os) (oddE ot) => sv1 tv1. set u := (s+t)./2; set v := (s-t)./2. have cp0: t < s. have qa: b ^ 2 - a ^ 2 <= b^2 by rewrite leq_subr. have qb: b ^ 2 < b ^ 2 + a ^ 2 by apply: ltn_paddr; rewrite expn_gt0 ap. by move: (leq_ltn_trans qa qb); rewrite t2 s2 ltn_sqr. have cp1: t./2 <= s./2 by apply: half_leq; apply:ltnW. have uE: u = s./2 + t./2 +1. by rewrite /u {1} sv1 {1}tv1 addSnnS -doubleS -doubleD doubleK addn1 addnS. have vE: v = s./2 - t./2. by rewrite /v {1} sv1 {1} tv1 subSS -doubleB doubleK. have sE: s = u + v. by rewrite uE vE addnAC -2!addnA (addnA t./2) subnKC //addnA addnn addn1. have tE: t = u - v. by rewrite uE vE (subnBA _ cp1) (addnAC s./2) -2!addnA addnn add1n -tv1 addKn. have luv: v < u by rewrite uE addn1 ltnS vE leq_BD. have cuv: coprime u v. move: cst; rewrite sE tE /coprime gcdnC -gcdnDl -addnA (subnKC (ltnW luv)). by rewrite addnn - muln2 Gauss_gcdl ? coprimen2 -?sE // sE gcdnC gcdnDl. have suv: u^2 + v ^2 = b^2. have h: (b^2).*2 = s^2 + t ^2 by rewrite -t2 -s2 -addnA (subnKC ha) addnn. apply/eqP; rewrite - eqn_double h sE tE sqrnD (sqrnB (ltnW luv)) -addnA. by rewrite subnKC ?addnn // nat_Cauchy. have puv: v * (2 * u) = a ^2. by move/eqP:(sqrnD u v);rewrite suv -sE -s2 eqn_add2l mulnA mulnC => /eqP ->. case: (posnP v) => vz; first by move: ap; rewrite - sqrn_gt0 -puv vz. case: (posnP u) => uz; first by move: luv; rewrite uz ltn0. case:(pythagore_tripleB suv). by move => []; rewrite uE addn1. by move => [vzz]; move: vz; rewrite vzz. move => [p [q [gp lqp cpq opq]]]; rewrite (eqP cuv) ! mul1n. have odf: odd (p ^ 2 - q ^ 2). by rewrite oddB ?odd_sqr ?leq_sqr ?(ltnW lqp) //= - negb_eqb. have pp: 0 < p by move: lqp; case p. have Hw w: 0 < w -> w <= w^2 by move => h; rewrite -{1}(expn1 w) leq_pexp2l. case=> [] [up vp bp]. case: (posnP q) => qp; first by move: vz; rewrite vp qp !muln0. have cp3: coprime u (2* v). by rewrite /coprime Gauss_gcdl // -/(coprime _ _) coprimen2 up. have puv': u * (2 * v) = a ^ 2 by rewrite - puv mulnCA mulnA mulnC. case:(factor_square uz cp3 puv'); set d := _ %/ _; set e := _ %/_. move => us vs cp4. move: (f_equal odd vs); rewrite odd_sqr mul2n odd_double => oe. move /eqP: vs; rewrite (evenE (esym oe)) - mul2n expnMn. rewrite vp - mulnA !mul2n 2! eqn_double => pqs. case: (factor_square pp cpq (eqP pqs)). set aa := _ %/ _; set bb := _ %/ _ => [Ha Hb Hc]. have bbp: 0 < bb by rewrite -sqrn_gt0 -Hb. have cba: bb < aa by rewrite -ltn_sqr -Ha -Hb. case: (posnP aa) => aap; first by move: cba; rewrite aap;case: (aa). have aaK: aa <= K. move: (Hw aa aap); rewrite -Ha => hb; apply: (leq_trans hb). rewrite -ltnS; apply: leq_trans ns. by apply:(leq_ltn_trans (Hw p pp)); rewrite bp ltn_paddr // sqrn_gt0. rewrite coprime_sym in Hc. by apply: (IH aa bb d aaK Hc) => //; rewrite -Ha -Hb -us up -subn_sqr. have cp3 : coprime v (2* u). by rewrite /coprime Gauss_gcdl 1? coprime_sym // -/(coprime _ _) coprimen2 up. case:(factor_square vz cp3 puv); set d:= _ %/ _; set e := _ %/ _ => us vs cp4. move: (f_equal odd vs); rewrite odd_sqr mul2n odd_double => oe. move /eqP: vs; rewrite (evenE (esym oe)) - mul2n expnMn -[2^2]/(2*2) - mulnA. rewrite vp !mul2n !eqn_double => pqs. case: (posnP q) => qp; first by move: uz; rewrite vp qp !muln0. case: (factor_square pp cpq (eqP pqs)). set aa := _ %/ _; set bb := _ %/ _ => [Ha Hb Hc]. have bbp: 0 < bb by rewrite -sqrn_gt0 -Hb. have cba: bb < aa by rewrite -ltn_sqr -Ha -Hb. case: (posnP aa) => aap; first by move: cba; rewrite aap;case: (aa). have aaK: aa <= K. move: (Hw aa aap); rewrite -Ha => hb; apply: (leq_trans hb). rewrite -ltnS; apply: leq_trans ns. by apply:(leq_ltn_trans (Hw p pp)); rewrite bp ltn_paddr // sqrn_gt0. rewrite coprime_sym in Hc. by apply: (IH aa bb d aaK Hc) => //; rewrite -Ha -Hb -us up -subn_sqr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)