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