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