Theorem: WithTop.add_coe_lt_add_iff (Jordan/Mathlib/Set.lean)

State before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ c + ↑m < ↑n + ↑m ↔ c < ↑n
Tactic:
rw [WithTop.add_lt_add_iff_right]
State after:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤

State before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤
Tactic:
exact WithTop.coe_ne_top
State after:
no goals