proposition: Lemma pythagore_tripleB x y z (r := gcdn x y): x^2 + y ^2 = z^2 -> [\/ x=0 /\ y = z, y = 0 /\ x = z | exists p q, [/\ 0 < r, q < p, coprime p q, odd p != odd q & [/\ x = r* (p^2 - q^2), y = r*(p*q).*2 & z = r*(p^2 + q ^2) ] \/ [/\ y = r* (p^2 - q^2), x = r*(p*q).*2 & z = r*(p^2 + q ^2) ]]].
proof: Proof. case: (posnP x) => xp. by move /eqP; rewrite xp add0n eqn_sqr => /eqP ->; constructor 1. case: (posnP y) => yp. by move /eqP; rewrite yp addn0 eqn_sqr => /eqP ->; constructor 2. move => h;constructor 3. case:(gcd_aux y xp); set a := _ %/ _; set b := _%/ _; rewrite -/r => xv yv cp1. have rp: 0 < r by rewrite gcdn_gt0 xp. move: h xp yp; rewrite xv yv !expnMn - mulnDl {xv yv}. move/(pythagore_aux rp); set c := z%/r; move => [-> h]. case az: (a==0); first by rewrite (eqP az) mul0n. case bz: (b==0); first by rewrite (eqP bz) mul0n. move => _ _; rewrite (mulnC a) (mulnC b) (mulnC c). wlog: a b az bz h cp1 / odd a && ~~(odd b). move => H; move: (pythagore_mod4 cp1 h). case oa: (odd a); first by move => /= ob; apply: H => //; rewrite oa ob. rewrite negb_eqb /= => /= ob; rewrite addnC in h; rewrite coprime_sym in cp1. have oc:odd b && ~~ odd a by rewrite oa ob. move:(H b a bz az h cp1 oc) =>[p [q [ha hb hc hd he]]];exists p,q. by split =>//;case: he => hh;[right| left]. move => /andP[oa eb]. have lac: a < c by rewrite - ltn_sqr -h ltn_paddr // expn_gt0 lt0n bz. have lac' := ltnW lac. move: (f_equal odd h); rewrite oddD ! odd_sqr oa (negbTE eb) /= => oc. have eq2:=(evenE (negbTE eb)). have eq3: b^2 = (c-a)* (c+a) by rewrite - subn_sqr -h addKn. move:(odd_double_half (c +a)); rewrite oddD oa - oc add0n => eq4. move:(odd_double_half (c -a)); rewrite oddB // oa - oc add0n => eq5. have eq6: (b./2) ^2 = (c - a)./2 * (c + a)./2. apply/eqP; rewrite -(@eqn_pmul2l (2 * 2)) // mulnACA !mul2n eq4 eq5 - eq3. by rewrite -(expnMn 2 _ 2) mul2n - eq2. have ap: 0 < a by rewrite lt0n az. have cp:=(ltn_trans ap lac). have cap: coprime c a. by rewrite -coprime_sqr -h coprime_sym coprimeDl coprime_sqr. case: (posnP (c - a)./2) => lt1. by move /eqP:eq6; rewrite lt1 expn_eq0 - double_eq0 -eq2 bz. have av: ((c + a)./2 - (c - a)./2) == a. by rewrite -eqn_double doubleB eq4 eq5 addnC -addnn -addnBA ?subKn// leq_subr. have cv: ((c - a)./2 + (c + a)./2) == c. by rewrite - eqn_double doubleD eq4 eq5 (addnC c) addnA (subnK lac') addnn. have lt2:= (leq_ltn_trans (leq_subr a c) (ltn_paddr c ap)). have cp2: (coprime (c - a)./2 (c + a)./2). move: (esym oc); rewrite -coprimen2 => hw. rewrite /coprime -gcdnDl (eqP cv) gcdnC -(Gauss_gcdr _ hw) mul2n eq5. by rewrite gcdnC -{2}(subnK lac') gcdnDl gcdnC - gcdnDr subnK // gcdnC. case: (factor_square lt1 cp2 (esym eq6)). set q := _ %/ _; set p := _ %/ _ => eq7 eq8 cpxy. have H w: odd w = odd (w ^2) by rewrite oddM andbb. have eq9: b = (p * q).*2. apply /eqP; rewrite -eqn_sqr - muln2 2!expnMn -eq8 -eq7 (mulnC (_ ./2)) -eq6. by rewrite - expnMn muln2 -eq2. exists p, q; rewrite - eq9 coprime_sym; split => //. + by rewrite - ltn_sqr -eq7 -eq8 - ltn_double eq4 eq5. + by rewrite (H p) (H q) negb_eqb -oddD -eq7 -eq8 addnC (eqP cv). + by left; rewrite -eq7 - eq8 (eqP av) addnC (eqP cv) eq9. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)