no goals
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
a b z : R
⊢ gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y
simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
  Ideal.mem_span_singleton]