α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ (f^[n]) x ≤ (f^[n]) (f x)
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ (f^[n]) x ≤ (f^[n + 1]) x
rw [iterate_succ_apply]
no goals
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ (f^[n]) x ≤ (f^[n]) (f x)
exact hf.iterate n hx