Interaction between successors and arithmetic

We define the SuccAddOrder and PredSubOrder typeclasses, for orders satisfying succ x = x + 1 and pred x = x - 1 respectively. This allows us to transfer the API for successors and predecessors into these common arithmetical forms.

Todo

In the future, we will make x + 1 and x - 1 the simp-normal forms for succ x and pred x respectively. This will require a refactor of Ordinal first, as the simp-normal form is currently set the other way around.

class SuccAddOrder (α : Type u_1) [Preorder α] [Add α] [One α] extends SuccOrder : Type u_1

A typeclass for succ x = x + 1.

• succ : α → α
• le_succ : ∀ (a : α), a ≤ SuccOrder.succ a
• max_of_succ_le : ∀ {a : α}, SuccOrder.succ a ≤ a → IsMax a
• succ_le_of_lt : ∀ {a b : α}, a < b → SuccOrder.succ a ≤ b
• succ_eq_add_one : ∀ (x : α), SuccOrder.succ x = x + 1

theorem SuccAddOrder.succ_eq_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [self : SuccAddOrder α] (x : α) : SuccOrder.succ x = x + 1

class PredSubOrder (α : Type u_1) [Preorder α] [Sub α] [One α] extends PredOrder : Type u_1

A typeclass for pred x = x - 1.

• pred : α → α
• pred_le : ∀ (a : α), PredOrder.pred a ≤ a
• min_of_le_pred : ∀ {a : α}, a ≤ PredOrder.pred a → IsMin a
• le_pred_of_lt : ∀ {a b : α}, a < b → a ≤ PredOrder.pred b
• pred_eq_sub_one : ∀ (x : α), PredOrder.pred x = x - 1

theorem PredSubOrder.pred_eq_sub_one {α : Type u_1} [Preorder α] [Sub α] [One α] [self : PredSubOrder α] (x : α) : PredOrder.pred x = x - 1

theorem Order.succ_eq_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] (x : α) : Order.succ x = x + 1

theorem Order.add_one_le_of_lt {α : Type u_1} {x : α} {y : α} [Preorder α] [Add α] [One α] [SuccAddOrder α] (h : x < y) : x + 1 ≤ y

theorem Order.add_one_le_iff_of_not_isMax {α : Type u_1} {x : α} {y : α} [Preorder α] [Add α] [One α] [SuccAddOrder α] (hx : ¬IsMax x) : x + 1 ≤ y ↔ x < y

theorem Order.add_one_le_iff {α : Type u_1} {x : α} {y : α} [Preorder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] : x + 1 ≤ y ↔ x < y

@[simp]

theorem Order.wcovBy_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] (x : α) : x ⩿ x + 1

@[simp]

theorem Order.covBy_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (x : α) : x ⋖ x + 1

theorem Order.pred_eq_sub_one {α : Type u_1} [Preorder α] [Sub α] [One α] [PredSubOrder α] (x : α) : Order.pred x = x - 1

theorem Order.le_sub_one_of_lt {α : Type u_1} {x : α} {y : α} [Preorder α] [Sub α] [One α] [PredSubOrder α] (h : x < y) : x ≤ y - 1

theorem Order.le_sub_one_iff_of_not_isMin {α : Type u_1} {x : α} {y : α} [Preorder α] [Sub α] [One α] [PredSubOrder α] (hy : ¬IsMin y) : x ≤ y - 1 ↔ x < y

theorem Order.le_sub_one_iff {α : Type u_1} {x : α} {y : α} [Preorder α] [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] : x ≤ y - 1 ↔ x < y

@[simp]

theorem Order.sub_one_wcovBy {α : Type u_1} [Preorder α] [Sub α] [One α] [PredSubOrder α] (x : α) : x - 1 ⩿ x

@[simp]

theorem Order.sub_one_covBy {α : Type u_1} [Preorder α] [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] (x : α) : x - 1 ⋖ x

@[simp]

theorem Order.succ_iterate {α : Type u_1} [Preorder α] [AddMonoidWithOne α] [SuccAddOrder α] (x : α) (n : ℕ) : Order.succ^[n] x = x + ↑n

@[simp]

theorem Order.pred_iterate {α : Type u_1} [Preorder α] [AddCommGroupWithOne α] [PredSubOrder α] (x : α) (n : ℕ) : Order.pred^[n] x = x - ↑n

theorem Order.not_isMax_zero {α : Type u_1} [PartialOrder α] [Zero α] [One α] [ZeroLEOneClass α] [NeZero 1] : ¬IsMax 0

theorem Order.one_le_iff_pos {α : Type u_1} {x : α} [PartialOrder α] [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero 1] [SuccAddOrder α] : 1 ≤ x ↔ 0 < x

theorem Order.covBy_iff_add_one_eq {α : Type u_1} {x : α} {y : α} [PartialOrder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] : x ⋖ y ↔ x + 1 = y

theorem Order.covBy_iff_sub_one_eq {α : Type u_1} {x : α} {y : α} [PartialOrder α] [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] : x ⋖ y ↔ y - 1 = x

theorem Order.le_of_lt_add_one {α : Type u_1} {x : α} {y : α} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] (h : x < y + 1) : x ≤ y

theorem Order.lt_add_one_iff_of_not_isMax {α : Type u_1} {x : α} {y : α} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] (hy : ¬IsMax y) : x < y + 1 ↔ x ≤ y

theorem Order.lt_add_one_iff {α : Type u_1} {x : α} {y : α} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] : x < y + 1 ↔ x ≤ y

theorem Order.le_of_sub_one_lt {α : Type u_1} {x : α} {y : α} [LinearOrder α] [Sub α] [One α] [PredSubOrder α] (h : x - 1 < y) : x ≤ y

theorem Order.sub_one_lt_iff_of_not_isMin {α : Type u_1} {x : α} {y : α} [LinearOrder α] [Sub α] [One α] [PredSubOrder α] (hx : ¬IsMin x) : x - 1 < y ↔ x ≤ y

theorem Order.sub_one_lt_iff {α : Type u_1} {x : α} {y : α} [LinearOrder α] [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] : x - 1 < y ↔ x ≤ y

theorem Order.lt_one_iff_nonpos {α : Type u_1} {x : α} [LinearOrder α] [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero 1] [SuccAddOrder α] : x < 1 ↔ x ≤ 0