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