α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ (f^[n]) x ≤ f ((f^[n]) x)
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ (f^[n]) x ≤ (f^[n + 1]) x
rw [iterate_succ_apply']
no goals
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ (f^[n]) x ≤ f ((f^[n]) x)
exact h _