Theorem: WithTop.add_one_lt_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_lt_add_iff]
State after:
no goals