R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
rw [isCoprime_comm] at h⊢
no goals
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x
exact h.of_add_mul_left_left