no goals
ι : Type ?u.45479
𝕜 : Type ?u.45482
R : Type u_1
M : Type u_2
N : Type ?u.45491
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
hc : 0 < c
⊢ 0 < c • a ↔ c • 0 < c • a
rw [smul_zero]