Helper theorems to assert constraints

theorem Lean.Grind.Order.eq_mp {p q : Prop} (h₁ : p = q) (h₂ : p) : q

theorem Lean.Grind.Order.eq_mp_not {p q : Prop} (h₁ : p = q) (h₂ : ¬p) : ¬q

theorem Lean.Grind.Order.eq_trans_true {p q : Prop} (h₁ : p = q) (h₂ : q = True) : p = True

theorem Lean.Grind.Order.eq_trans_false {p q : Prop} (h₁ : p = q) (h₂ : q = False) : p = False

theorem Lean.Grind.Order.eq_trans_true' {p q : Prop} (h₁ : p = q) (h₂ : p = True) : q = True

theorem Lean.Grind.Order.eq_trans_false' {p q : Prop} (h₁ : p = q) (h₂ : p = False) : q = False

theorem Lean.Grind.Order.le_of_eq_1 {α : Type u_1} [LE α] [Std.IsPreorder α] {a b : α} : a = b → a ≤ b

theorem Lean.Grind.Order.le_of_eq_2 {α : Type u_1} [LE α] [Std.IsPreorder α] {a b : α} : a = b → b ≤ a

theorem Lean.Grind.Order.le_of_eq_1_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} : a = b → a ≤ b + ↑0

theorem Lean.Grind.Order.le_of_eq_2_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} : a = b → b ≤ a + ↑0

theorem Lean.Grind.Order.le_of_offset_eq_1_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} {k : Int} : a = b + ↑k → a ≤ b + ↑k

theorem Lean.Grind.Order.le_of_offset_eq_2_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} {k : Int} : a = b + ↑k → b ≤ a + ↑(-k)

theorem Lean.Grind.Order.nat_eq (a b : Nat) (x y : Int) : ↑a = x → ↑b = y → x = y → a = b

theorem Lean.Grind.Order.of_nat_eq (a b : Nat) (x y : Int) : ↑a = x → ↑b = y → a = b → x = y

theorem Lean.Grind.Order.le_of_not_le {α : Type u_1} [LE α] [Std.IsLinearPreorder α] {a b : α} : ¬a ≤ b → b ≤ a

theorem Lean.Grind.Order.lt_of_not_le {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] {a b : α} : ¬a ≤ b → b < a

theorem Lean.Grind.Order.le_of_not_lt {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] {a b : α} : ¬a < b → b ≤ a

theorem Lean.Grind.Order.le_of_not_lt_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] [Ring α] [OrderedRing α] {a b : α} {k k' : Int} : k'.beq' (-k) = true → ¬a < b + ↑k → b ≤ a + ↑k'

theorem Lean.Grind.Order.lt_of_not_le_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] [Ring α] [OrderedRing α] {a b : α} {k k' : Int} : k'.beq' (-k) = true → ¬a ≤ b + ↑k → b < a + ↑k'

theorem Lean.Grind.Order.int_lt {x y k k' : Int} : k'.beq' (k - 1) = true → x < y + k → x ≤ y + k'

Helper theorem for equality propagation

theorem Lean.Grind.Order.eq_of_le_of_le {α : Type u_1} [LE α] [Std.IsPartialOrder α] {a b : α} : a ≤ b → b ≤ a → a = b

theorem Lean.Grind.Order.eq_of_le_of_le_0 {α : Type u_1} [LE α] [Std.IsPartialOrder α] [Ring α] {a b : α} : a ≤ b + ↑0 → b ≤ a + ↑0 → a = b

Transitivity

theorem Lean.Grind.Order.le_trans {α : Type u_1} [LE α] [Std.IsPreorder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c

theorem Lean.Grind.Order.lt_trans {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a < b) (h₂ : b < c) : a < c

theorem Lean.Grind.Order.le_lt_trans {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c

theorem Lean.Grind.Order.lt_le_trans {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) : a < c

theorem Lean.Grind.Order.lt_unsat {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] (a : α) : a < a → False

Transitivity with offsets

theorem Lean.Grind.Order.le_trans_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b c : α} {k₁ k₂ : Int} (k : Int) (h₁ : a ≤ b + ↑k₁) (h₂ : b ≤ c + ↑k₂) : (k == k₂ + k₁) = true → a ≤ c + ↑k

theorem Lean.Grind.Order.lt_trans_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b c : α} {k₁ k₂ : Int} (k : Int) (h₁ : a < b + ↑k₁) (h₂ : b < c + ↑k₂) : (k == k₂ + k₁) = true → a < c + ↑k

theorem Lean.Grind.Order.le_lt_trans_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b c : α} {k₁ k₂ : Int} (k : Int) (h₁ : a ≤ b + ↑k₁) (h₂ : b < c + ↑k₂) : (k == k₂ + k₁) = true → a < c + ↑k

theorem Lean.Grind.Order.lt_le_trans_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b c : α} {k₁ k₂ : Int} (k : Int) (h₁ : a < b + ↑k₁) (h₂ : b ≤ c + ↑k₂) : (k == k₂ + k₁) = true → a < c + ↑k

Unsat detection

theorem Lean.Grind.Order.le_unsat_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a : α} {k : Int} : k.blt' 0 = true → a ≤ a + ↑k → False

theorem Lean.Grind.Order.lt_unsat_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a : α} {k : Int} : k.ble' 0 = true → a < a + ↑k → False

Helper theorems

Theorems for propagating constraints to True

theorem Lean.Grind.Order.le_eq_true_of_lt {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] {a b : α} : a < b → (a ≤ b) = True

theorem Lean.Grind.Order.le_eq_true {α : Type u_1} [LE α] [Std.IsPreorder α] {a : α} : (a ≤ a) = True

theorem Lean.Grind.Order.le_eq_true_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a : α} {k : Int} : Int.ble' 0 k = true → (a ≤ a + ↑k) = True

theorem Lean.Grind.Order.lt_eq_true_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a : α} {k : Int} : Int.blt' 0 k = true → (a < a + ↑k) = True

theorem Lean.Grind.Order.le_eq_true_of_le_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} {k₁ k₂ : Int} : k₁.ble' k₂ = true → a ≤ b + ↑k₁ → (a ≤ b + ↑k₂) = True

theorem Lean.Grind.Order.le_eq_true_of_lt_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} {k₁ k₂ : Int} : k₁.ble' k₂ = true → a < b + ↑k₁ → (a ≤ b + ↑k₂) = True

theorem Lean.Grind.Order.lt_eq_true_of_lt_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} {k₁ k₂ : Int} : k₁.ble' k₂ = true → a < b + ↑k₁ → (a < b + ↑k₂) = True

theorem Lean.Grind.Order.lt_eq_true_of_le_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} {k₁ k₂ : Int} : k₁.blt' k₂ = true → a ≤ b + ↑k₁ → (a < b + ↑k₂) = True

Theorems for propagating constraints to False

theorem Lean.Grind.Order.lt_eq_false {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] {a : α} : (a < a) = False

theorem Lean.Grind.Order.le_eq_false_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a : α} {k : Int} : k.blt' 0 = true → (a ≤ a + ↑k) = False

theorem Lean.Grind.Order.lt_eq_false_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a : α} {k : Int} : k.ble' 0 = true → (a < a + ↑k) = False

theorem Lean.Grind.Order.le_eq_false_of_lt {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α} : a < b → (b ≤ a) = False

theorem Lean.Grind.Order.lt_eq_false_of_lt {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α} : a < b → (b < a) = False

theorem Lean.Grind.Order.lt_eq_false_of_le {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α} : a ≤ b → (b < a) = False

theorem Lean.Grind.Order.le_eq_false_of_le_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] {a b : α} {k₁ k₂ : Int} : (k₂ + k₁).blt' 0 = true → a ≤ b + ↑k₁ → (b ≤ a + ↑k₂) = False

theorem Lean.Grind.Order.lt_eq_false_of_le_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] (a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 = true → a ≤ b + ↑k₁ → (b < a + ↑k₂) = False

theorem Lean.Grind.Order.lt_eq_false_of_lt_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] (a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 = true → a < b + ↑k₁ → (b < a + ↑k₂) = False

theorem Lean.Grind.Order.le_eq_false_of_lt_k {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] (a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 = true → a < b + ↑k₁ → (b ≤ a + ↑k₂) = False