r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r * r + s * s) r
r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r ^ 2 + s ^ 2) r
rw [sq, sq]
no goals
r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r * r + s * s) r
exact (IsCoprime.mul_left h2 h2).mul_add_left_left r