proposition: Lemma pythagore_tripleA p q r (x := r* (p^2 - q^2)) (y := r*(p*q).*2) (z:= r*(p^2 + q ^2)): q <= p -> x^2 + y^2 = z ^2.
proof: Proof. rewrite /x /y/z -leq_sqr /= !expnMn -mulnDr -mul2n !expnMn => h. rewrite -(sqrnD_sub h) subnK //; apply:nat_AGM2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)