k : Type u_2
M : Type u_1
N : Type ?u.12824
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a ≤ b
hc : c ≤ 0
⊢ -c • a ≤ -c • b
k : Type u_2
M : Type u_1
N : Type ?u.12824
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a ≤ b
hc : c ≤ 0
⊢ c • b ≤ c • a
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff]
no goals
k : Type u_2
M : Type u_1
N : Type ?u.12824
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a ≤ b
hc : c ≤ 0
⊢ -c • a ≤ -c • b
exact smul_le_smul_of_nonneg h (neg_nonneg_of_nonpos hc)