α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, (succ^[n]) a = b) → a ≤ b
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, (succ^[n]) a = b) ↔ a ≤ b
refine' ⟨_, exists_succ_iterate_of_le⟩
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a : α
n : ℕ
⊢ a ≤ (succ^[n]) a
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, (succ^[n]) a = b) → a ≤ b
rintro ⟨n, rfl⟩
no goals
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a : α
n : ℕ
⊢ a ≤ (succ^[n]) a
exact id_le_iterate_of_id_le le_succ n a