α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
C : α → Sort ?u.8730
inst✝ : NoMaxOrder α
⊢ (∃ x, succ x = a) ↔ a ∈ range succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
C : α → Sort ?u.8730
inst✝ : NoMaxOrder α
⊢ ¬IsSuccLimit a ↔ a ∈ range succ
simp_rw [isSuccLimit_iff_succ_ne, not_forall, not_ne_iff]
no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
C : α → Sort ?u.8730
inst✝ : NoMaxOrder α
⊢ (∃ x, succ x = a) ↔ a ∈ range succ
rfl