no goals
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.26709
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.26791
inst✝ : DecidableEq ι
x y z : M
r : R
h : SameRay R x y
hr : 0 ≤ r
hy : y = 0
⊢ r • y = 0
rw [hy, smul_zero]