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

State before:
α : Type u_1
c : ℕ∞
n : ℕ
⊢ c + 1 ≤ ↑(Nat.succ n) ↔ c ≤ ↑n
Tactic:
rw [← Nat.cast_one, Nat.succ_eq_add_one, Nat.cast_add, WithTop.add_coe_le_add_iff]
State after:
no goals