k : Type u_1
M : Type u_2
N : Type ?u.2442
inst✝³ : OrderedSemiring k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : 0 < c
⊢ 0 < c • -a ↔ 0 < -a
k : Type u_1
M : Type u_2
N : Type ?u.2442
inst✝³ : OrderedSemiring k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : 0 < c
⊢ c • a < 0 ↔ a < 0
rw [← neg_neg a, smul_neg, neg_neg_iff_pos, neg_neg_iff_pos]
no goals
k : Type u_1
M : Type u_2
N : Type ?u.2442
inst✝³ : OrderedSemiring k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : 0 < c
⊢ 0 < c • -a ↔ 0 < -a
exact smul_pos_iff_of_pos hc