proposition: Lemma square_plus_square_3square x y z: x^2 + y^2 = 3 * z ^2 -> z = 0.
proof: Proof. wlog: x y/ y <= x. by move => H; case/orP: (leq_total y x); [| rewrite addnC]; apply:H. case: (posnP x) => xp. rewrite xp leqn0 => /eqP -> /eqP; rewrite eq_sym muln_eq0 expn_eq0 /=. by rewrite andbT => /eqP. case (gcd_aux y xp); set a := _ %/ _; set b := _ %/ _. move => {3} -> {3} ->. rewrite !expnMn -mulnDl => cp _ eqa. case: (posnP z) => //; rewrite -sqrn_gt0 => zp. have /(logn_Gauss ((gcdn x y) ^2)): coprime 3 (a ^ 2 + b ^ 2). move: (dvdn_gcd 3 a b). rewrite (eqP cp) /= /dvdn /coprime -gcdn_modr -modnDm - modnMm - (modnMm b). move: (@ltn_pmod a 3 isT); move: (@ltn_pmod b 3 isT). case:(a %% 3) => [|[|[]]];case:(b %% 3) => [|[|[]]] => //. rewrite eqa lognM // logn_prime // !lognX => H. by move: (f_equal odd H); rewrite !mul2n add1n /= !odd_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)