x y : ℝ*
⊢ InfinitePos (-x) → ¬InfiniteNeg (-y) → InfinitePos (-x + -y)
x y : ℝ*
⊢ InfiniteNeg x → ¬InfinitePos y → InfiniteNeg (x + y)
rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]
no goals
x y : ℝ*
⊢ InfinitePos (-x) → ¬InfiniteNeg (-y) → InfinitePos (-x + -y)
exact infinitePos_add_not_infiniteNeg