proposition: Lemma pythagore_gcd p q: q <= p -> coprime p q -> odd p != odd q -> coprime (p ^ 2 - q ^ 2) (p * q).*2.
proof: Proof. move => lqp; rewrite {2}/coprime. rewrite subn_sqr -{1 2 4 5} (subnK lqp); set r := p - q. rewrite /coprime_sym /coprime gcdnC gcdnDr -/(coprime _ _) => cqr. rewrite oddD negb_eqb - addbA addbb addbF => or. have cpq: (coprime (r * (r + q + q)) q). by rewrite coprime_sym /coprime Gauss_gcdr // !gcdnDr. have cp2: coprime (r * (r + q + q)) 2. by rewrite /coprime gcd_n2 oddM - addnA oddD or addnn odd_double. rewrite - mul2n Gauss_gcdr // Gauss_gcdl // gcdnC Gauss_gcdl. by rewrite gcdnC -/(coprime _ _) coprimeDl coprime_sym. by rewrite coprimeDl coprime_sym coprimeDr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)