x y : ℝ*
hx : ¬Infinitesimal x
hp : 0 < x
hy : InfiniteNeg y
⊢ InfiniteNeg (y * x)
x y : ℝ*
hx : ¬Infinitesimal x
hp : 0 < x
hy : InfiniteNeg y
⊢ InfiniteNeg (x * y)
rw [mul_comm]
no goals
x y : ℝ*
hx : ¬Infinitesimal x
hp : 0 < x
hy : InfiniteNeg y
⊢ InfiniteNeg (y * x)
exact infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hy hx hp