mathlib3

8de08f72 - chore(order/iterate): generalize lemmas about inequalities and iterations (#5357)

chore(order/iterate): generalize lemmas about inequalities and iterations (#5357) If `f : α → α` is a monotone function and `x y : ℕ → α` are two sequences such that `x 0 ≤ y 0`, `x (n + 1) ≤ f (x n)`, and `f (y n) ≤ y (n + 1)`, then `x n ≤ y n`. This lemma (and its versions for `<`) generalize `geom_le` as well as `iterate_le_of_map_le`.