Iteration of a function which doesn't decrease values

Stream: Is there code for X?

[Daniel Weber]

Is this lemma in Mathlib?

lemma le_iterate_of_forall_le {α : Type*} [Preorder α] (f : α → α)
    (hf : ∀ x, x ≤ f x) (x : α) (n : ℕ) :
    x ≤ f^[n] x := by
  induction n generalizing x
  · simp
  · trans f x
    · apply hf
    · simp only [iterate_succ, comp_apply, *]

I also need the corollary

lemma monotone_iterate_of_forall_le {α : Type*} [Preorder α] (f : α → α)
    (hf : ∀ x, x ≤ f x) (x : α) :
    Monotone (fun n ↦ f^[n] x)

[Yury G. Kudryashov]

@loogle Monotone, Nat.iterate, "id_le"

[loogle]

:search: Function.monotone_iterate_of_id_le

[Daniel Weber]

Thanks