no goals
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J K : Submodule R A
⊢ I ≤ J / K ↔ I * K ≤ J
rw [le_div_iff, mul_le]