α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
⊢ (id^[k]) x ≤ (succ^[k]) x
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
⊢ x ≤ (succ^[k]) x
conv_lhs => rw [(by simp only [Function.iterate_id, id.def] : x = (id^[k]) x)]
no goals
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
⊢ (id^[k]) x ≤ (succ^[k]) x
exact Monotone.le_iterate_of_le succ_mono le_succ k x
no goals
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
k : ℕ
x : α
⊢ x = (id^[k]) x
simp only [Function.iterate_id, id.def]