r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) s
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) (r * s)
apply IsCoprime.mul_right (Int.coprime_of_sq_sum (isCoprime_comm.mp h))
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (s ^ 2 + r ^ 2) s
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) s
rw [add_comm]
no goals
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (s ^ 2 + r ^ 2) s
apply Int.coprime_of_sq_sum h