no goals
R : Type u
ι : Type ?u.238401
inst✝¹ : CommSemiring R
I J K L : Ideal R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ I * span {x} ≤ J * span {x} ↔ I ≤ J
simpa only [mul_comm I, mul_comm J] using span_singleton_mul_right_mono hx