x y : ℝ*
⊢ InfinitePos (-x) → ¬Infinitesimal y → 0 < y → InfinitePos (-x * y)
x y : ℝ*
⊢ InfiniteNeg x → ¬Infinitesimal y → 0 < y → InfiniteNeg (x * y)
rw [← infinitePos_neg, ← infinitePos_neg, neg_mul_eq_neg_mul]
no goals
x y : ℝ*
⊢ InfinitePos (-x) → ¬Infinitesimal y → 0 < y → InfinitePos (-x * y)
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos