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 r4p:0 < r ^ (2 * 2) by rewrite expn_gt0 rp. have: (r^2)^2 %| x ^2 by rewrite eqb /dvdn modnMl. rewrite dvdn_pexp2r // => /dvdnP [c xv]. move /eqP: eqa; rewrite sa sb xv !expnMn mulnn - expnM -mulnDl eqn_pmul2r //. rewrite -[4]/(2*2) 2!expnM => /eqP eqc. have cpp: coprime c (a^2). by rewrite -coprime_sqr coprime_sym -coprimeDr eqc !coprime_sqr. move: (Fermat4_alt eqc cpp); set W:= (or3 _ _ _) => H. have wt: W by constructor 2; split; [ exists a| exists b]; left. move: (H wt); case/orP => ea. by move: xp; rewrite xv (eqP ea). by move: ea yp; rewrite expn_eq0 andbT sa => /eqP ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)