theorem Lean.Grind.Preorder.le_of_lt {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] {a b : α} (h : a < b) : a ≤ b

theorem Lean.Grind.Preorder.lt_irrefl {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] (a : α) : ¬a < a

theorem Lean.Grind.Preorder.ne_of_lt {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] {a b : α} (h : a < b) : a ≠ b

theorem Lean.Grind.Preorder.ne_of_gt {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] {a b : α} (h : a > b) : a ≠ b

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

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

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

theorem Lean.Grind.Preorder.not_ge_of_lt {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α} (h : a < b) : ¬b ≤ a

theorem Lean.Grind.Preorder.not_gt_of_lt {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α} (h : a < b) : ¬a > b

theorem Lean.Grind.PartialOrder.le_iff_lt_or_eq {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPartialOrder α] {a b : α} : a ≤ b ↔ a < b ∨ a = b

theorem Lean.Grind.LinearOrder.trichotomy {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] (a b : α) : a < b ∨ a = b ∨ b < a

theorem Lean.Grind.LinearOrder.le_of_not_lt {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {a b : α} (h : ¬a < b) : b ≤ a

theorem Lean.Grind.LinearOrder.lt_of_not_le {α : Type u} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {a b : α} (h : ¬a ≤ b) : b < a