no goals
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
a b : R
H : a * (x + y * z) + b * y = 1
⊢ a * x + (a * z + b) * y = 1
simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm,
  mul_left_comm] using H