k : Type u_2
M : Type u_1
N : Type ?u.17203
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hab : -c • a = -c • b
hc : c < 0
h : a ≤ b
⊢ a = b
k : Type u_2
M : Type u_1
N : Type ?u.17203
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hab : c • a = c • b
hc : c < 0
h : a ≤ b
⊢ a = b
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_inj] at hab
no goals
k : Type u_2
M : Type u_1
N : Type ?u.17203
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hab : -c • a = -c • b
hc : c < 0
h : a ≤ b
⊢ a = b
exact eq_of_smul_eq_smul_of_pos_of_le hab (neg_pos_of_neg hc) h