α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
⊢ (pred^[k]) x ≤ (id^[k]) x
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
⊢ (pred^[k]) x ≤ x
conv_rhs => rw [(by simp only [Function.iterate_id, id.def] : x = (id^[k]) x)]
no goals
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
⊢ (pred^[k]) x ≤ (id^[k]) x
exact Monotone.iterate_le_of_le pred_mono pred_le k x
no goals
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
k : ℕ
x : α
⊢ x = (id^[k]) x
simp only [Function.iterate_id, id.def]