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