no goals
ι : Type ?u.113737
𝕜 : Type u_1
R : Type ?u.113743
M : Type u_2
N : Type ?u.113749
inst✝⁵ : LinearOrderedSemifield 𝕜
inst✝⁴ : OrderedAddCommMonoid M
inst✝³ : OrderedAddCommMonoid N
inst✝² : MulActionWithZero 𝕜 M
inst✝¹ : MulActionWithZero 𝕜 N
inst✝ : OrderedSMul 𝕜 M
s : Set M
a b : M
c : 𝕜
h : 0 < c
⊢ a ≤ c⁻¹ • b ↔ c • a ≤ b
rw [← smul_le_smul_iff_of_pos h, smul_inv_smul₀ h.ne']