no goals
k : Type u_1
M : Type u_2
N : Type ?u.102476
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ a < c⁻¹ • b ↔ b < c • a
rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne]