Comparing iterated successors

In a successor order, succ^[n] a is the element n steps above a. This file compares such iterates. Without a maximal element, applying the same number of further steps preserves and reflects the order, and an element at least n steps above a lies strictly above every iterate succ^[m] a with m < n. An element b ≥ a that is none of a, succ a, …, succ^[n - 1] a lies at least n steps above a.

These comparisons measure how far apart two elements of a discrete order are, up to a bound, as in the Ehrenfeucht–Fraïssé analysis of discrete linear orders.

theorem Order.succ_iterate_lt_succ_iterate_of_succ_iterate_le {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] {a b : α} {n m : ℕ} (h : succ^[n] a ≤ b) (hm : m < n) (k : ℕ) : succ^[m] a < succ^[k] b

If b lies at least n successor steps above a, then fewer than n steps above a lies strictly below any number of steps above b.

theorem Order.succ_iterate_add_le_succ_iterate_add_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] {a b : α} (m n k : ℕ) : succ^[m + k] a ≤ succ^[n + k] b ↔ succ^[m] a ≤ succ^[n] b

In a linear order without a maximal element, taking k further successor steps on both sides preserves and reflects the order.

theorem Order.succ_iterate_le_of_forall_ne {α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} (hab : a ≤ b) {n : ℕ} (hne : ∀ k < n, succ^[k] a ≠ b) : succ^[n] a ≤ b

An element b ≥ a that is none of a, succ a, …, succ^[n - 1] a lies at least n successor steps above a.