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

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