no goals
α : Type u
β : Type v
a b : α
inst✝² : CommSemiring α
I : Ideal α
inst✝¹ : CommRing β
inst✝ : IsDomain β
x y : β
⊢ span {x} < span {y} ↔ DvdNotUnit y x
rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
  dvd_and_not_dvd_iff]