diff --git a/src/Init/Data/Int/Compare.lean b/src/Init/Data/Int/Compare.lean
new file mode 100644
index 0000000000..4bd45f0d81
--- /dev/null
+++ b/src/Init/Data/Int/Compare.lean
@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert
+-/
+prelude
+import Init.Data.Ord
+import Init.Data.Int.Order
+
+/-! # Basic lemmas about comparing integers
+
+This file introduces some basic lemmas about `compare` as applied to integers.
+
+Import `Std.Classes.Ord` in order to obtain the `TransOrd` and `LawfulEqOrd` instances for `Int`.
+-/
+namespace Int
+
+protected theorem lt_or_eq_of_le {n m : Int} (h : n ≤ m) : n < m ∨ n = m := by
+  omega
+
+protected theorem le_iff_lt_or_eq {n m : Int} : n ≤ m ↔ n < m ∨ n = m :=
+  ⟨Int.lt_or_eq_of_le, fun | .inl h => Int.le_of_lt h | .inr rfl => Int.le_refl _⟩
+
+theorem compare_eq_ite_lt (a b : Int) :
+    compare a b = if a < b then .lt else if b < a then .gt else .eq := by
+  simp only [compare, compareOfLessAndEq]
+  split
+  · rfl
+  · next h =>
+    match Int.lt_or_eq_of_le (Int.not_lt.1 h) with
+    | .inl h => simp [h, Int.ne_of_gt h]
+    | .inr rfl => simp
+
+theorem compare_eq_ite_le (a b : Int) :
+    compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt := by
+  rw [compare_eq_ite_lt]
+  split
+  · next hlt => simp [Int.le_of_lt hlt, Int.not_le.2 hlt]
+  · next hge =>
+    split
+    · next hgt => simp [Int.le_of_lt hgt, Int.not_le.2 hgt]
+    · next hle => simp [Int.not_lt.1 hge, Int.not_lt.1 hle]
+
+protected theorem compare_swap (a b : Int) : (compare a b).swap = compare b a := by
+  simp only [compare_eq_ite_le]; (repeat' split) <;> try rfl
+  next h1 h2 => cases h1 (Int.le_of_not_le h2)
+
+protected theorem compare_eq_eq {a b : Int} : compare a b = .eq ↔ a = b := by
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [Int.ne_of_lt, Int.ne_of_gt, *]
+  next hlt hgt => exact Int.le_antisymm (Int.not_lt.1 hgt) (Int.not_lt.1 hlt)
+
+protected theorem compare_eq_lt {a b : Int} : compare a b = .lt ↔ a < b := by
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [*]
+
+protected theorem compare_eq_gt {a b : Int} : compare a b = .gt ↔ b < a := by
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [Int.le_of_lt, *]
+
+protected theorem compare_ne_gt {a b : Int} : compare a b ≠ .gt ↔ a ≤ b := by
+  rw [compare_eq_ite_le]; (repeat' split) <;> simp [*]
+
+protected theorem compare_ne_lt {a b : Int} : compare a b ≠ .lt ↔ b ≤ a := by
+  rw [compare_eq_ite_le]; (repeat' split) <;> simp [Int.le_of_not_le, *]
+
+protected theorem isLE_compare {a b : Int} :
+    (compare a b).isLE ↔ a ≤ b := by
+  simp only [Int.compare_eq_ite_le]
+  repeat' split <;> simp_all
+
+protected theorem isGE_compare {a b : Int} :
+    (compare a b).isGE ↔ b ≤ a := by
+  rw [← Int.compare_swap, Ordering.isGE_swap]
+  exact Int.isLE_compare
+
+end Int
diff --git a/src/Init/Data/Nat/Compare.lean b/src/Init/Data/Nat/Compare.lean
index 27914b4233..3736ae9ab5 100644
--- a/src/Init/Data/Nat/Compare.lean
+++ b/src/Init/Data/Nat/Compare.lean
@@ -4,17 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
-import Init.Classical
 import Init.Data.Ord
 
 /-! # Basic lemmas about comparing natural numbers
 
 This file introduce some basic lemmas about compare as applied to natural
 numbers.
+
+Import `Std.Classes.Ord` in order to obtain the `TransOrd` and `LawfulEqOrd` instances for `Nat`.
 -/
 namespace Nat
 
-theorem compare_def_lt (a b : Nat) :
+theorem compare_eq_ite_lt (a b : Nat) :
     compare a b = if a < b then .lt else if b < a then .gt else .eq := by
   simp only [compare, compareOfLessAndEq]
   split
@@ -24,9 +25,12 @@ theorem compare_def_lt (a b : Nat) :
     | .inl h => simp [h, Nat.ne_of_gt h]
     | .inr rfl => simp
 
-theorem compare_def_le (a b : Nat) :
+@[deprecated compare_eq_ite_lt (since := "2025-03_28")]
+def compare_def_lt := compare_eq_ite_lt
+
+theorem compare_eq_ite_le (a b : Nat) :
     compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt := by
-  rw [compare_def_lt]
+  rw [compare_eq_ite_lt]
   split
   · next hlt => simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt]
   · next hge =>
@@ -34,24 +38,37 @@ theorem compare_def_le (a b : Nat) :
     · next hgt => simp [Nat.le_of_lt hgt, Nat.not_le.2 hgt]
     · next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle]
 
+@[deprecated compare_eq_ite_le (since := "2025-03_28")]
+def compare_def_le := compare_eq_ite_le
+
 protected theorem compare_swap (a b : Nat) : (compare a b).swap = compare b a := by
-  simp only [compare_def_le]; (repeat' split) <;> try rfl
+  simp only [compare_eq_ite_le]; (repeat' split) <;> try rfl
   next h1 h2 => cases h1 (Nat.le_of_not_le h2)
 
 protected theorem compare_eq_eq {a b : Nat} : compare a b = .eq ↔ a = b := by
-  rw [compare_def_lt]; (repeat' split) <;> simp [Nat.ne_of_lt, Nat.ne_of_gt, *]
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [Nat.ne_of_lt, Nat.ne_of_gt, *]
   next hlt hgt => exact Nat.le_antisymm (Nat.not_lt.1 hgt) (Nat.not_lt.1 hlt)
 
 protected theorem compare_eq_lt {a b : Nat} : compare a b = .lt ↔ a < b := by
-  rw [compare_def_lt]; (repeat' split) <;> simp [*]
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [*]
 
 protected theorem compare_eq_gt {a b : Nat} : compare a b = .gt ↔ b < a := by
-  rw [compare_def_lt]; (repeat' split) <;> simp [Nat.le_of_lt, *]
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [Nat.le_of_lt, *]
 
 protected theorem compare_ne_gt {a b : Nat} : compare a b ≠ .gt ↔ a ≤ b := by
-  rw [compare_def_le]; (repeat' split) <;> simp [*]
+  rw [compare_eq_ite_le]; (repeat' split) <;> simp [*]
 
 protected theorem compare_ne_lt {a b : Nat} : compare a b ≠ .lt ↔ b ≤ a := by
-  rw [compare_def_le]; (repeat' split) <;> simp [Nat.le_of_not_le, *]
+  rw [compare_eq_ite_le]; (repeat' split) <;> simp [Nat.le_of_not_le, *]
+
+protected theorem isLE_compare {a b : Nat} :
+    (compare a b).isLE ↔ a ≤ b := by
+  simp only [Nat.compare_eq_ite_le]
+  repeat' split <;> simp_all
+
+protected theorem isGE_compare {a b : Nat} :
+    (compare a b).isGE ↔ b ≤ a := by
+  rw [← Nat.compare_swap, Ordering.isGE_swap]
+  exact Nat.isLE_compare
 
 end Nat
diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index 540d7c90b6..67f1c396ba 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -304,6 +304,27 @@ theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq 
 theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by
   cases o₁ <;> cases o₂ <;> decide
 
+@[simp]
+theorem lt_then {o : Ordering} : lt.then o = lt := rfl
+
+@[simp]
+theorem gt_then {o : Ordering} : gt.then o = gt := rfl
+
+@[simp]
+theorem eq_then {o : Ordering} : eq.then o = o := rfl
+
+theorem isLE_then_iff_or {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂.isLE) := by
+  cases o₁ <;> simp
+
+theorem isLE_then_iff_and {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁.isLE ∧ (o₁ = lt ∨ o₂.isLE) := by
+  cases o₁ <;> simp
+
+theorem isLE_left_of_isLE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isLE) : o₁.isLE := by
+  cases o₁ <;> simp_all
+
+theorem isGE_left_of_isGE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isGE) : o₁.isGE := by
+  cases o₁ <;> simp_all
+
 end Lemmas
 
 end Ordering
@@ -345,6 +366,104 @@ To lexicographically combine two `Ordering`s, use `Ordering.then`.
 @[inline] def compareLex (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering :=
   (cmp₁ a b).then (cmp₂ a b)
 
+section Lemmas
+
+@[simp]
+theorem compareLex_eq_eq {α} {cmp₁ cmp₂} {a b : α} :
+    compareLex cmp₁ cmp₂ a b = .eq ↔ cmp₁ a b = .eq ∧ cmp₂ a b = .eq := by
+  simp [compareLex, Ordering.then_eq_eq]
+
+theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
+    (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) {x y : α} :
+    compareOfLessAndEq x y = (compareOfLessAndEq y x).swap := by
+  simp only [compareOfLessAndEq]
+  split
+  · rename_i h'
+    rw [h] at h'
+    simp only [h'.1, h'.2.symm, reduceIte, Ordering.swap_gt]
+  · split
+    · rename_i h'
+      have : ¬ y < y := Not.imp (·.2 rfl) <| (h y y).mp
+      simp only [h', this, reduceIte, Ordering.swap_eq]
+    · rename_i h' h''
+      replace h' := (h y x).mpr ⟨h', Ne.symm h''⟩
+      simp only [h', Ne.symm h'', reduceIte, Ordering.swap_lt]
+
+theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (x y : α) :
+    x < y ↔ ¬ y < x ∧ x ≠ y := by
+  simp only [← not_le, Classical.not_not]
+  constructor
+  · intro h
+    have refl := by cases total y y <;> assumption
+    exact ⟨(total _ _).resolve_left h, fun h' => (h' ▸ h) refl⟩
+  · intro ⟨h₁, h₂⟩ h₃
+    exact h₂ (antisymm h₁ h₃)
+
+theorem compareOfLessAndEq_eq_swap
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) {x y : α} :
+    compareOfLessAndEq x y = (compareOfLessAndEq y x).swap := by
+  apply compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne
+  exact lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le antisymm total not_le
+
+@[simp]
+theorem compareOfLessAndEq_eq_lt
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} :
+    compareOfLessAndEq x y = .lt ↔ x < y := by
+  rw [compareOfLessAndEq]
+  repeat' split <;> simp_all
+
+theorem compareOfLessAndEq_eq_eq
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
+    (refl : ∀ (x : α), x ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) {x y : α} :
+    compareOfLessAndEq x y = .eq ↔ x = y := by
+  rw [compareOfLessAndEq]
+  repeat' split <;> try (simp_all; done)
+  simp only [reduceCtorEq, false_iff]
+  rintro rfl
+  rename_i hlt
+  simp [← not_le] at hlt
+  exact hlt (refl x)
+
+theorem compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α}
+    (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) :
+    compareOfLessAndEq x y = .gt ↔ y < x := by
+  rw [compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne h, Ordering.swap_eq_gt]
+  exact compareOfLessAndEq_eq_lt
+
+theorem compareOfLessAndEq_eq_gt
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (x y : α) :
+    compareOfLessAndEq x y = .gt ↔ y < x := by
+  apply compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne
+  exact lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le antisymm total not_le
+
+theorem isLE_compareOfLessAndEq
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) {x y : α} :
+    (compareOfLessAndEq x y).isLE ↔ x ≤ y := by
+  have refl (a : α) := by cases total a a <;> assumption
+  rw [Ordering.isLE_iff_eq_lt_or_eq_eq, compareOfLessAndEq_eq_lt,
+    compareOfLessAndEq_eq_eq refl not_le]
+  constructor
+  · rintro (h | rfl)
+    · rw [← not_le] at h
+      exact total _ _ |>.resolve_left h
+    · exact refl x
+  · intro hle
+    by_cases hge : x ≥ y
+    · exact Or.inr <| antisymm hle hge
+    · exact Or.inl <| not_le.mp hge
+
+end Lemmas
+
 /--
 `Ord α` provides a computable total order on `α`, in terms of the
 `compare : α → α → Ordering` function.
diff --git a/src/Std/Classes/Ord.lean b/src/Std/Classes/Ord.lean
index 11fc932429..3e40bf387c 100644
--- a/src/Std/Classes/Ord.lean
+++ b/src/Std/Classes/Ord.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel, Paul Reichert
+Authors: Markus Himmel, Paul Reichert, Robin Arnez
 -/
 prelude
 import Init.Data.Ord
@@ -66,6 +66,9 @@ abbrev OrientedOrd (α : Type u) [Ord α] := OrientedCmp (compare : α → α 
 
 variable {α : Type u} {cmp : α → α → Ordering}
 
+theorem OrientedOrd.eq_swap [Ord α] [OrientedOrd α] {a b : α} :
+    compare a b = (compare b a).swap := OrientedCmp.eq_swap
+
 instance [OrientedCmp cmp] : ReflCmp cmp where
   compare_self := Ordering.eq_eq_of_eq_swap OrientedCmp.eq_swap
 
@@ -104,12 +107,12 @@ theorem OrientedCmp.eq_symm [OrientedCmp cmp] {a b : α} : cmp a b = .eq → cmp
   OrientedCmp.eq_comm.1
 
 theorem OrientedCmp.not_isLE_of_lt [OrientedCmp cmp] {a b : α} :
-    cmp a b = .lt → ¬(cmp b a).isLE := by
+    cmp a b = .lt → ¬ (cmp b a).isLE := by
   rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
   simp
 
 theorem OrientedCmp.not_isGE_of_gt [OrientedCmp cmp] {a b : α} :
-    cmp a b = .gt → ¬(cmp b a).isGE := by
+    cmp a b = .gt → ¬ (cmp b a).isGE := by
   rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
   simp
 
@@ -134,12 +137,12 @@ theorem OrientedCmp.not_gt_of_gt [OrientedCmp cmp] {a b : α} :
   cases cmp b a <;> simp
 
 theorem OrientedCmp.lt_of_not_isLE [OrientedCmp cmp] {a b : α} :
-    ¬(cmp a b).isLE → cmp b a = .lt := by
+    ¬ (cmp a b).isLE → cmp b a = .lt := by
   rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
   cases cmp b a <;> simp
 
 theorem OrientedCmp.gt_of_not_isGE [OrientedCmp cmp] {a b : α} :
-    ¬(cmp a b).isGE → cmp b a = .gt := by
+    ¬ (cmp a b).isGE → cmp b a = .gt := by
   rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
   cases cmp b a <;> simp
 
@@ -157,11 +160,19 @@ abbrev TransOrd (α : Type u) [Ord α] := TransCmp (compare : α → α → Orde
 
 variable {α : Type u} {cmp : α → α → Ordering}
 
+theorem TransOrd.isLE_trans [Ord α] [TransOrd α] {a b c : α} :
+    (compare a b).isLE → (compare b c).isLE → (compare a c).isLE :=
+  TransCmp.isLE_trans
+
 theorem TransCmp.isGE_trans [TransCmp cmp] {a b c : α} (h₁ : (cmp a b).isGE) (h₂ : (cmp b c).isGE) :
     (cmp a c).isGE := by
   rw [OrientedCmp.isGE_iff_isLE] at *
   exact TransCmp.isLE_trans h₂ h₁
 
+theorem TransOrd.isGE_trans [Ord α] [TransOrd α] {a b c : α} :
+    (compare a b).isGE → (compare b c).isGE → (compare a c).isGE :=
+  TransCmp.isGE_trans
+
 instance TransCmp.opposite [TransCmp cmp] : TransCmp fun a b => cmp b a where
   isLE_trans := flip TransCmp.isLE_trans
 
@@ -228,6 +239,10 @@ theorem TransCmp.gt_of_gt_of_isGE [TransCmp cmp] {a b c : α} (hab : cmp a b = .
   rw [OrientedCmp.gt_iff_lt, OrientedCmp.isGE_iff_isLE] at *
   exact TransCmp.lt_of_isLE_of_lt hbc hab
 
+theorem TransCmp.gt_of_gt_of_gt [TransCmp cmp] {a b c : α} (hab : cmp a b = .gt)
+    (hbc : cmp b c = .gt) : cmp a c = .gt := by
+  apply gt_of_gt_of_isGE hab (Ordering.isGE_of_eq_gt hbc)
+
 theorem TransCmp.gt_of_isGE_of_gt [TransCmp cmp] {a b c : α} (hab : (cmp a b).isGE)
     (hbc : cmp b c = .gt) : cmp a c = .gt := by
   rw [OrientedCmp.gt_iff_lt, OrientedCmp.isGE_iff_isLE] at *
@@ -295,6 +310,9 @@ abbrev LawfulEqOrd (α : Type u) [Ord α] := LawfulEqCmp (compare : α → α 
 
 variable {α : Type u} {cmp : α → α → Ordering} [LawfulEqCmp cmp]
 
+theorem LawfulEqOrd.eq_of_compare [Ord α] [LawfulEqOrd α] {a b : α} :
+    compare a b = .eq → a = b := LawfulEqCmp.eq_of_compare
+
 instance LawfulEqCmp.opposite [OrientedCmp cmp] [LawfulEqCmp cmp] :
     LawfulEqCmp (fun a b => cmp b a) where
   eq_of_compare := by
@@ -435,4 +453,249 @@ theorem lawfulBEq_of_lawfulEqOrd [Ord α] [LawfulEqOrd α] : LawfulBEq α where
 
 end Internal
 
+section Instances
+
+theorem TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff
+    {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
+    (lt_trans : ∀ {a b c : α}, a < b → b < c → a < c)
+    (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) :
+    TransCmp (fun x y : α => compareOfLessAndEq x y) where
+  eq_swap := compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne h
+  isLE_trans {x y z} h₁ h₂ := by
+    simp only [compare, compareOfLessAndEq, apply_ite Ordering.isLE,
+      Ordering.isLE_lt, Ordering.isLE_eq, Ordering.isLE_gt] at h₁ h₂ ⊢
+    simp only [Bool.if_true_left, Bool.or_false, Bool.or_eq_true, decide_eq_true_eq] at h₁ h₂ ⊢
+    rcases h₁ with (h₁ | rfl)
+    · rcases h₂ with (h₂ | rfl)
+      · exact .inl (lt_trans h₁ h₂)
+      · exact .inl h₁
+    · exact h₂
+
+theorem TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (trans : ∀ {x y z : α}, x ≤ y → y ≤ z → x ≤ z) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x)
+    (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) :
+    TransCmp (fun x y : α => compareOfLessAndEq x y) := by
+  refine compareOfLessAndEq_of_lt_trans_of_lt_iff ?_ ?_
+  · intro a b c
+    simp only [← not_le]
+    intro h₁ h₂ h₃
+    replace h₁ := (total _ _).resolve_left h₁
+    exact h₂ (trans h₃ h₁)
+  · exact lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le antisymm total not_le
+
+namespace Bool
+
+instance : TransOrd Bool where
+  eq_swap {x y} := by cases x <;> cases y <;> rfl
+  isLE_trans {x y z} h₁ h₂ := by cases x <;> cases y <;> cases z <;> trivial
+
+instance : LawfulEqOrd Bool where
+  eq_of_compare {x y} := by cases x <;> cases y <;> simp
+
+end Bool
+
+namespace Nat
+
+instance : TransOrd Nat :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    Nat.le_antisymm Nat.le_trans Nat.le_total Nat.not_le
+
+instance : LawfulEqOrd Nat where
+  eq_of_compare := compareOfLessAndEq_eq_eq Nat.le_refl Nat.not_le |>.mp
+
+end Nat
+
+namespace Int
+
+instance : TransOrd Int :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    Int.le_antisymm Int.le_trans Int.le_total Int.not_le
+
+instance : LawfulEqOrd Int where
+  eq_of_compare := compareOfLessAndEq_eq_eq Int.le_refl Int.not_le |>.mp
+
+end Int
+
+namespace Fin
+
+variable (n : Nat)
+
+instance : OrientedOrd (Fin n) where
+  eq_swap := OrientedOrd.eq_swap (α := Nat)
+
+instance : TransOrd (Fin n) where
+  isLE_trans := TransOrd.isLE_trans (α := Nat)
+
+instance : LawfulEqOrd (Fin n) where
+  eq_of_compare h := Fin.eq_of_val_eq <| LawfulEqOrd.eq_of_compare h
+
+end Fin
+
+namespace String
+
+instance : TransOrd String :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    String.le_antisymm String.le_trans String.le_total String.not_le
+
+instance : LawfulEqOrd String where
+  eq_of_compare h := compareOfLessAndEq_eq_eq String.le_refl String.not_le |>.mp h
+
+end String
+
+namespace Char
+
+instance : TransOrd Char :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    Char.le_antisymm Char.le_trans Char.le_total Char.not_le
+
+instance : LawfulEqOrd Char where
+  eq_of_compare h := compareOfLessAndEq_eq_eq Char.le_refl Char.not_le |>.mp h
+
+end Char
+
+namespace UInt8
+
+instance : TransOrd UInt8 :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    UInt8.le_antisymm UInt8.le_trans UInt8.le_total UInt8.not_le
+
+instance : LawfulEqOrd UInt8 where
+  eq_of_compare h := compareOfLessAndEq_eq_eq UInt8.le_refl UInt8.not_le |>.mp h
+
+end UInt8
+
+namespace UInt16
+
+instance : TransOrd UInt16 :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    UInt16.le_antisymm UInt16.le_trans UInt16.le_total UInt16.not_le
+
+instance : LawfulEqOrd UInt16 where
+  eq_of_compare h := compareOfLessAndEq_eq_eq UInt16.le_refl UInt16.not_le |>.mp h
+
+end UInt16
+
+namespace UInt32
+
+instance : TransOrd UInt32 :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    UInt32.le_antisymm UInt32.le_trans UInt32.le_total UInt32.not_le
+
+instance : LawfulEqOrd UInt32 where
+  eq_of_compare h := compareOfLessAndEq_eq_eq UInt32.le_refl UInt32.not_le |>.mp h
+
+end UInt32
+
+namespace UInt64
+
+instance : TransOrd UInt64 :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    UInt64.le_antisymm UInt64.le_trans UInt64.le_total UInt64.not_le
+
+instance : LawfulEqOrd UInt64 where
+  eq_of_compare h := compareOfLessAndEq_eq_eq UInt64.le_refl UInt64.not_le |>.mp h
+
+end UInt64
+
+namespace USize
+
+instance : TransOrd USize :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    USize.le_antisymm USize.le_trans USize.le_total USize.not_le
+
+instance : LawfulEqOrd USize where
+  eq_of_compare h := compareOfLessAndEq_eq_eq USize.le_refl USize.not_le |>.mp h
+
+end USize
+
+namespace Option
+
+instance {α} [Ord α] [OrientedOrd α] : OrientedOrd (Option α) where
+  eq_swap {a b} := by cases a <;> cases b <;> simp [Ord.compare, ← OrientedOrd.eq_swap]
+
+instance {α} [Ord α] [TransOrd α] : TransOrd (Option α) where
+  isLE_trans {a b c} hab hbc := by
+    cases a <;> cases b <;> cases c <;> (try simp_all [Ord.compare]; done)
+    simp only [Ord.compare] at *
+    apply TransOrd.isLE_trans <;> assumption
+
+instance {α} [Ord α] [ReflOrd α] : ReflOrd (Option α) where
+  compare_self {a} := by cases a <;> simp [Ord.compare]
+
+instance {α} [Ord α] [LawfulEqOrd α] : LawfulEqOrd (Option α) where
+  eq_of_compare {a b} := by
+    cases a <;> cases b <;> simp_all [Ord.compare, LawfulEqOrd.eq_of_compare]
+
+instance {α} [Ord α] [BEq α] [LawfulBEqOrd α] : LawfulBEqOrd (Option α) where
+  compare_eq_iff_beq {a b} := by
+    cases a <;> cases b <;> simp_all [Ord.compare, LawfulBEqOrd.compare_eq_iff_beq]
+
+end Option
+
+section Lex
+
+instance {α} {cmp₁ cmp₂} [ReflCmp cmp₁] [ReflCmp cmp₂] :
+    ReflCmp (α := α) (compareLex cmp₁ cmp₂) where
+  compare_self {a} := by simp [compareLex, ReflCmp.compare_self]
+
+instance {α} {cmp₁ cmp₂} [OrientedCmp cmp₁] [OrientedCmp cmp₂] :
+    OrientedCmp (α := α) (compareLex cmp₁ cmp₂) where
+  eq_swap {a b} := by
+    rw [compareLex, compareLex, OrientedCmp.eq_swap (cmp := cmp₁) (a := b), Ordering.swap_then,
+      Ordering.swap_swap, ← OrientedCmp.eq_swap]
+
+instance {α} {cmp₁ cmp₂} [TransCmp cmp₁] [TransCmp cmp₂] :
+    TransCmp (α := α) (compareLex cmp₁ cmp₂) where
+  isLE_trans {a b c} hab hbc := by
+    simp only [compareLex] at *
+    simp only [Ordering.isLE_then_iff_and] at *
+    refine ⟨TransCmp.isLE_trans hab.1 hbc.1, ?_⟩
+    cases hab.2
+    case inl hab' => exact Or.inl <| TransCmp.lt_of_lt_of_isLE hab' hbc.1
+    case inr hab' =>
+      cases hbc.2
+      case inl hbc' => exact Or.inl <| TransCmp.lt_of_isLE_of_lt hab.1 hbc'
+      case inr hbc' => exact Or.inr <| TransCmp.isLE_trans hab' hbc'
+
+instance {α β} {f : α → β} [Ord β] [ReflOrd β] :
+    ReflCmp (compareOn f) where
+  compare_self := ReflOrd.compare_self (α := β)
+
+instance {α β} {f : α → β} [Ord β] [OrientedOrd β] :
+    OrientedCmp (compareOn f) where
+  eq_swap := OrientedOrd.eq_swap (α := β)
+
+instance {α β} {f : α → β} [Ord β] [TransOrd β] :
+    TransCmp (compareOn f) where
+  isLE_trans := TransOrd.isLE_trans (α := β)
+
+attribute [instance] lexOrd in
+instance {α β} [Ord α] [Ord β] [ReflOrd α] [ReflOrd β] :
+    ReflOrd (α × β) :=
+  inferInstanceAs <| ReflCmp (compareLex _ _)
+
+attribute [instance] lexOrd in
+instance {α β} [Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] :
+    OrientedOrd (α × β) :=
+  inferInstanceAs <| OrientedCmp (compareLex _ _)
+
+attribute [instance] lexOrd in
+instance {α β} [Ord α] [Ord β] [TransOrd α] [TransOrd β] :
+    TransOrd (α × β) :=
+  inferInstanceAs <| TransCmp (compareLex _ _)
+
+attribute [instance] lexOrd in
+instance {α β} [Ord α] [Ord β] [LawfulEqOrd α] [LawfulEqOrd β] : LawfulEqOrd (α × β) where
+  eq_of_compare {a b} h := by
+    simp only [lexOrd, compareLex_eq_eq, compareOn] at h
+    ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2
+
+end Lex
+
+end Instances
+
 end Std
diff --git a/src/Std/Time/Date/PlainDate.lean b/src/Std/Time/Date/PlainDate.lean
index a85f3d0c11..03ebbace23 100644
--- a/src/Std/Time/Date/PlainDate.lean
+++ b/src/Std/Time/Date/PlainDate.lean
@@ -21,6 +21,7 @@ set_option linter.all true
 `PlainDate` represents a date in the Year-Month-Day (YMD) format. It encapsulates the year, month,
 and day components, with validation to ensure the date is valid.
 -/
+@[ext]
 structure PlainDate where
 
   /-- The year component of the date. It is represented as an `Offset` type from `Year`. -/
@@ -34,13 +35,27 @@ structure PlainDate where
 
   /-- Validates the date by ensuring that the year, month, and day form a correct and valid date. -/
   valid : year.Valid month day
-  deriving Repr
+deriving Repr, DecidableEq
 
 instance : Inhabited PlainDate where
   default := ⟨1, 1, 1, by decide⟩
 
-instance : BEq PlainDate where
-  beq x y := x.day == y.day && x.month == y.month && x.year == y.year
+instance : Ord PlainDate where
+  compare := compareLex (compareOn (·.year)) <| compareLex (compareOn (·.month)) (compareOn (·.day))
+
+theorem PlainDate.compare_def :
+    compare (α := PlainDate) =
+      compareLex (compareOn (·.year)) (compareLex (compareOn (·.month)) (compareOn (·.day))) := rfl
+
+instance : TransOrd PlainDate := inferInstanceAs <| TransCmp (compareLex _ _)
+
+instance : LawfulEqOrd PlainDate where
+  eq_of_compare {a b} h := by
+    simp only [PlainDate.compare_def, compareLex_eq_eq] at h
+    ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2.1
+    · exact LawfulEqOrd.eq_of_compare h.2.2
 
 namespace PlainDate
 
diff --git a/src/Std/Time/Date/Unit/Day.lean b/src/Std/Time/Date/Unit/Day.lean
index 9020ea068b..03e8ac1204 100644
--- a/src/Std/Time/Date/Unit/Day.lean
+++ b/src/Std/Time/Date/Unit/Day.lean
@@ -17,7 +17,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for days, which ranges between 1 and 31.
 -/
 def Ordinal := Bounded.LE 1 31
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
 
 instance : OfNat Ordinal n :=
   inferInstanceAs (OfNat (Bounded.LE 1 (1 + (30 : Nat))) n)
@@ -30,12 +30,18 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 
 instance : Inhabited Ordinal where default := 1
 
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 /--
 `Offset` represents an offset in days. It is defined as an `Int` with a base unit of 86400
 (the number of seconds in a day).
 -/
 def Offset : Type := UnitVal 86400
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
 instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩
 
@@ -45,6 +51,12 @@ instance {x y : Offset} : Decidable (x ≤ y) :=
 instance {x y : Offset} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Ordinal
 
 /--
@@ -66,6 +78,14 @@ instance : Repr (OfYear leap) where
 instance : ToString (OfYear leap) where
   toString r := toString r.val
 
+instance : DecidableEq (OfYear leap) := inferInstanceAs <| DecidableEq (Bounded.LE 1 _)
+
+instance : Ord (OfYear leap) := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd (OfYear leap) := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd (OfYear leap) := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 namespace OfYear
 
 /--
diff --git a/src/Std/Time/Date/Unit/Month.lean b/src/Std/Time/Date/Unit/Month.lean
index 9a5796a1fa..afb3a014ba 100644
--- a/src/Std/Time/Date/Unit/Month.lean
+++ b/src/Std/Time/Date/Unit/Month.lean
@@ -19,7 +19,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for months, which ranges between 1 and 12.
 -/
 def Ordinal := Bounded.LE 1 12
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
 
 instance : OfNat Ordinal n :=
   inferInstanceAs (OfNat (Bounded.LE 1 (1 + (11 : Nat))) n)
@@ -33,11 +33,17 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 /--
 `Offset` represents an offset in months. It is defined as an `Int`.
 -/
 def Offset : Type := Int
-  deriving Repr, BEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE, DecidableEq
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE
 
 instance {x y : Offset} : Decidable (x ≤ y) :=
   Int.decLe x y
@@ -48,10 +54,28 @@ instance {x y : Offset} : Decidable (x < y) :=
 instance : OfNat Offset n :=
   ⟨Int.ofNat n⟩
 
+instance : Ord Offset := inferInstanceAs <| Ord Int
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd Int
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd Int
+
 /--
 `Quarter` represents a value between 1 and 4, inclusive, corresponding to the four quarters of a year.
 -/
 def Quarter := Bounded.LE 1 4
+deriving Repr, DecidableEq, LT, LE
+
+instance : OfNat Quarter n := inferInstanceAs <| OfNat (Bounded.LE 1 (1 + (3 : Nat))) n
+
+instance : Inhabited Quarter where
+  default := 1
+
+instance : Ord Quarter := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Quarter := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Quarter := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
 
 namespace Quarter
 
diff --git a/src/Std/Time/Date/Unit/Week.lean b/src/Std/Time/Date/Unit/Week.lean
index fd23dc8432..8918938629 100644
--- a/src/Std/Time/Date/Unit/Week.lean
+++ b/src/Std/Time/Date/Unit/Week.lean
@@ -19,7 +19,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for weeks, which ranges between 1 and 53.
 -/
 def Ordinal := Bounded.LE 1 53
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
 
 instance : OfNat Ordinal n :=
   inferInstanceAs (OfNat (Bounded.LE 1 (1 + (52 : Nat))) n)
@@ -33,11 +33,17 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 instance : Inhabited Ordinal where
   default := 1
 
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 /--
 `Offset` represents an offset in weeks.
 -/
 def Offset : Type := UnitVal (86400 * 7)
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
 instance {x y : Offset} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
@@ -47,6 +53,12 @@ instance {x y : Offset} : Decidable (x < y) :=
 
 instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩
 
+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Ordinal
 
 /--
@@ -61,7 +73,18 @@ def ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 53) : Ordinal :=
 correct bounds—either 1 to 6, representing the possible weeks in a month.
 -/
 def OfMonth := Bounded.LE 1 6
-  deriving Repr
+deriving Repr, DecidableEq
+
+instance : OfNat OfMonth n := inferInstanceAs (OfNat (Bounded.LE 1 (1 + (5 : Nat))) n)
+
+instance : Inhabited OfMonth where
+  default := 1
+
+instance : Ord OfMonth := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd OfMonth := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd OfMonth := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
 
 /--
 Creates an `Ordinal` from a natural number, ensuring the value is within bounds.
diff --git a/src/Std/Time/Date/Unit/Weekday.lean b/src/Std/Time/Date/Unit/Weekday.lean
index 14c90848a8..48f73d4478 100644
--- a/src/Std/Time/Date/Unit/Weekday.lean
+++ b/src/Std/Time/Date/Unit/Weekday.lean
@@ -38,7 +38,7 @@ inductive Weekday
 
     /-- Sunday. -/
   | sunday
-  deriving Repr, Inhabited, BEq
+deriving Repr, Inhabited, DecidableEq
 
 namespace Weekday
 
@@ -46,10 +46,26 @@ namespace Weekday
 `Ordinal` represents a bounded value for weekdays, which ranges between 1 and 7.
 -/
 def Ordinal := Bounded.LE 1 7
+deriving Repr, DecidableEq, LT, LE
+
+instance {x y : Ordinal} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Ordinal} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Ordinal n :=
   inferInstanceAs (OfNat (Bounded.LE 1 (1 + (6 : Nat))) n)
 
+instance : Inhabited Ordinal where
+  default := 1
+
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 /--
 Converts a `Ordinal` representing a day index into a corresponding `Weekday`. This function is useful
 for mapping numerical representations to days of the week.
@@ -75,6 +91,17 @@ def toOrdinal : Weekday → Ordinal
   | .saturday => 6
   | .sunday => 7
 
+instance : Ord Weekday where
+  compare := compareOn toOrdinal
+
+instance : TransOrd Weekday := inferInstanceAs <| TransCmp (compareOn toOrdinal)
+
+theorem toOrdinal.inj {a b : Weekday} (h : toOrdinal a = toOrdinal b) : a = b := by
+  cases a <;> cases b <;> rw [toOrdinal] at * <;> contradiction
+
+instance : LawfulEqOrd Weekday where
+  eq_of_compare := toOrdinal.inj ∘ LawfulEqOrd.eq_of_compare (α := Ordinal)
+
 /--
 Converts a `Weekday` to a `Nat`.
 -/
diff --git a/src/Std/Time/Date/Unit/Year.lean b/src/Std/Time/Date/Unit/Year.lean
index eef7c2010c..fcc9289271 100644
--- a/src/Std/Time/Date/Unit/Year.lean
+++ b/src/Std/Time/Date/Unit/Year.lean
@@ -26,7 +26,7 @@ inductive Era
 
   /-- The Common Era (CE), represents dates from year 0 onwards. -/
   | ce
-  deriving Repr, Inhabited
+deriving Repr, Inhabited
 
 instance : ToString Era where
   toString
@@ -37,7 +37,7 @@ instance : ToString Era where
 `Offset` represents a year offset, defined as an `Int`.
 -/
 def Offset : Type := Int
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
 instance {x y : Offset} : Decidable (x ≤ y) :=
   let x : Int := x
@@ -49,6 +49,12 @@ instance {x y : Offset} : Decidable (x < y) :=
 
 instance : OfNat Offset n := ⟨Int.ofNat n⟩
 
+instance : Ord Offset := inferInstanceAs <| Ord Int
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd Int
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd Int
+
 namespace Offset
 
 /--
diff --git a/src/Std/Time/Date/ValidDate.lean b/src/Std/Time/Date/ValidDate.lean
index ce74efb4ee..70794e2501 100644
--- a/src/Std/Time/Date/ValidDate.lean
+++ b/src/Std/Time/Date/ValidDate.lean
@@ -25,6 +25,20 @@ def ValidDate (leap : Bool) := { val : Month.Ordinal × Day.Ordinal // Valid lea
 instance : Inhabited (ValidDate l) where
   default := ⟨⟨1, 1⟩, (by cases l <;> decide)⟩
 
+instance : DecidableEq (ValidDate leap) := Subtype.instDecidableEq
+
+instance : Ord (ValidDate leap) where
+  compare a b := compare a.val b.val
+
+instance : OrientedOrd (ValidDate leap) where
+  eq_swap := OrientedOrd.eq_swap (α := Month.Ordinal × Day.Ordinal)
+
+instance : TransOrd (ValidDate leap) where
+  isLE_trans := TransOrd.isLE_trans (α := Month.Ordinal × Day.Ordinal)
+
+instance : LawfulEqOrd (ValidDate leap) where
+  eq_of_compare := Subtype.ext ∘ LawfulEqOrd.eq_of_compare (α := Month.Ordinal × Day.Ordinal)
+
 namespace ValidDate
 
 /--
diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean
index 787238ce9f..8f39c9926f 100644
--- a/src/Std/Time/DateTime/PlainDateTime.lean
+++ b/src/Std/Time/DateTime/PlainDateTime.lean
@@ -18,6 +18,7 @@ set_option linter.all true
 /--
 Represents a date and time with components for Year, Month, Day, Hour, Minute, Second, and Nanosecond.
 -/
+@[ext]
 structure PlainDateTime where
 
   /--
@@ -29,7 +30,22 @@ structure PlainDateTime where
   The `Time` component of a `PlainTime`
   -/
   time : PlainTime
-  deriving Inhabited, BEq, Repr
+deriving Inhabited, DecidableEq, Repr
+
+instance : Ord PlainDateTime where
+  compare := compareLex (compareOn (·.date)) (compareOn (·.time))
+
+theorem PlainDateTime.compare_def :
+    compare (α := PlainDateTime) = compareLex (compareOn (·.date)) (compareOn (·.time)) := rfl
+
+instance : TransOrd PlainDateTime := inferInstanceAs <| TransCmp (compareLex _ _)
+
+instance : LawfulEqOrd PlainDateTime where
+  eq_of_compare {a b} h := by
+    simp only [PlainDateTime.compare_def, compareLex_eq_eq] at h
+    apply PlainDateTime.ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2
 
 namespace PlainDateTime
 
diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean
index 713ebcd3a9..b4976450f5 100644
--- a/src/Std/Time/DateTime/Timestamp.lean
+++ b/src/Std/Time/DateTime/Timestamp.lean
@@ -19,13 +19,14 @@ set_option linter.all true
 /--
 Represents an exact point in time as a UNIX Epoch timestamp.
 -/
+@[ext]
 structure Timestamp where
 
   /--
   Duration since the unix epoch.
   -/
   val : Duration
-  deriving Repr, BEq, Inhabited
+deriving Repr, DecidableEq, Inhabited
 
 instance : LE Timestamp where
   le x y := x.val ≤ y.val
@@ -42,6 +43,20 @@ instance : ToString Timestamp where
 instance : Repr Timestamp where
   reprPrec s := Repr.addAppParen ("Timestamp.ofNanosecondsSinceUnixEpoch " ++ repr s.val.toNanoseconds)
 
+instance : Ord Timestamp where
+  compare := compareOn (·.val)
+
+theorem Timestamp.compare_def :
+    compare (α := Timestamp) = compareOn (·.val) := rfl
+
+instance : TransOrd Timestamp := inferInstanceAs <| TransCmp (compareOn _)
+
+instance : LawfulEqOrd Timestamp where
+  eq_of_compare {a b} h := by
+    simp only [Timestamp.compare_def] at h
+    apply Timestamp.ext
+    exact LawfulEqOrd.eq_of_compare h
+
 namespace Timestamp
 
 /--
diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean
index 8560ae6124..d5ddb5b42a 100644
--- a/src/Std/Time/Duration.lean
+++ b/src/Std/Time/Duration.lean
@@ -16,6 +16,7 @@ set_option linter.all true
 /--
 Represents a time interval with nanoseconds precision.
 -/
+@[ext]
 structure Duration where
 
   /--
@@ -32,7 +33,7 @@ structure Duration where
   Proof that the duration is valid, ensuring that the `second` and `nano` values are correctly related.
   -/
   proof : (second.val ≥ 0 ∧ nano.val ≥ 0) ∨ (second.val ≤ 0 ∧ nano.val ≤ 0)
-  deriving Repr
+deriving Repr, DecidableEq
 
 instance : ToString Duration where
   toString s :=
@@ -47,9 +48,6 @@ instance : ToString Duration where
 instance : Repr Duration where
   reprPrec s := reprPrec (toString s)
 
-instance : BEq Duration where
-  beq x y := x.second == y.second && y.nano == x.nano
-
 instance : Inhabited Duration where
   default := ⟨0, Bounded.LE.mk 0 (by decide), by decide⟩
 
@@ -58,6 +56,21 @@ instance : OfNat Duration n where
     refine ⟨.ofInt n, ⟨0, by decide⟩, ?_⟩
     simp <;> exact Int.le_total n 0 |>.symm
 
+instance : Ord Duration where
+  compare := compareLex (compareOn (·.second)) (compareOn (·.nano))
+
+theorem Duration.compare_def :
+    compare (α := Duration) = compareLex (compareOn (·.second)) (compareOn (·.nano)) := rfl
+
+instance : TransOrd Duration := inferInstanceAs <| TransCmp (compareLex _ _)
+
+instance : LawfulEqOrd Duration where
+  eq_of_compare {a b} h := by
+    simp only [Duration.compare_def, compareLex_eq_eq] at h
+    ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2
+
 namespace Duration
 
 /--
diff --git a/src/Std/Time/Internal/Bounded.lean b/src/Std/Time/Internal/Bounded.lean
index 7c6bd29038..c5ff135cb6 100644
--- a/src/Std/Time/Internal/Bounded.lean
+++ b/src/Std/Time/Internal/Bounded.lean
@@ -6,6 +6,7 @@ Authors: Sofia Rodrigues
 prelude
 import Init.Omega
 import Init.Data.Int.DivMod.Lemmas
+import Std.Classes.Ord
 
 namespace Std
 namespace Time
@@ -29,18 +30,32 @@ instance : LE (Bounded rel n m) where
 instance : LT (Bounded rel n m) where
   lt l r := l.val < r.val
 
+@[always_inline]
+instance : Ord (Bounded rel n m) where
+  compare := compareOn (·.val)
+
 @[always_inline]
 instance : Repr (Bounded rel m n) where
   reprPrec n := reprPrec n.val
 
 @[always_inline]
-instance : BEq (Bounded rel n m) where
-  beq x y := (x.val = y.val)
+instance : DecidableEq (Bounded rel n m) := Subtype.instDecidableEq
 
 @[always_inline]
 instance {x y : Bounded rel a b} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
+instance : OrientedOrd (Bounded rel n m) where
+  eq_swap := OrientedOrd.eq_swap (α := Int)
+
+instance : TransOrd (Bounded rel n m) where
+  isLE_trans := TransOrd.isLE_trans (α := Int)
+
+instance : LawfulEqOrd (Bounded rel n m) where
+  eq_of_compare := Subtype.ext ∘ LawfulEqOrd.eq_of_compare (α := Int)
+
+variable {rel a b}
+
 /--
 A `Bounded` integer that the relation used is the the less-equal relation so, it includes all
 integers that `lo ≤ val ≤ hi`.
diff --git a/src/Std/Time/Internal/UnitVal.lean b/src/Std/Time/Internal/UnitVal.lean
index 2013bbaf3b..633d66547a 100644
--- a/src/Std/Time/Internal/UnitVal.lean
+++ b/src/Std/Time/Internal/UnitVal.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
+import Std.Classes.Ord
 import Std.Internal.Rat
 
 namespace Std
@@ -17,6 +18,7 @@ set_option linter.all true
 /--
 A structure representing a unit of a given ratio type `α`.
 -/
+@[ext]
 structure UnitVal (α : Rat) where
   /--
   Creates a `UnitVal` from an `Int`.
@@ -27,12 +29,27 @@ structure UnitVal (α : Rat) where
   Value inside the UnitVal Value.
   -/
   val : Int
-  deriving Inhabited, BEq
+deriving Inhabited, DecidableEq
 
 instance : LE (UnitVal x) where
   le x y := x.val ≤ y.val
 
-instance { x y : UnitVal z }: Decidable (x ≤ y) :=
+instance : Ord (UnitVal x) where
+  compare x y := compare x.val y.val
+
+theorem UnitVal.compare_def {x} {a b : UnitVal x} :
+    compare a b = compare a.1 b.1 := by rfl
+
+instance : OrientedOrd (UnitVal x) where
+  eq_swap := OrientedOrd.eq_swap (α := Int)
+
+instance : TransOrd (UnitVal x) where
+  isLE_trans := TransOrd.isLE_trans (α := Int)
+
+instance : LawfulEqOrd (UnitVal x) where
+  eq_of_compare := UnitVal.ext ∘ LawfulEqOrd.eq_of_compare (α := Int)
+
+instance {x y : UnitVal z}: Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
 namespace UnitVal
diff --git a/src/Std/Time/Time/HourMarker.lean b/src/Std/Time/Time/HourMarker.lean
index 0a05dd1613..dea8b47833 100644
--- a/src/Std/Time/Time/HourMarker.lean
+++ b/src/Std/Time/Time/HourMarker.lean
@@ -27,7 +27,23 @@ inductive HourMarker
   Post meridiem.
   -/
   | pm
-  deriving Repr, BEq
+deriving Repr, DecidableEq
+
+instance : Ord HourMarker where
+  compare
+    | .am, .am => .eq
+    | .am, .pm => .lt
+    | .pm, .am => .gt
+    | .pm, .pm => .eq
+
+instance : OrientedOrd HourMarker where
+  eq_swap {a b} := by cases a <;> cases b <;> rfl
+
+instance : TransOrd HourMarker where
+  isLE_trans {a b c} hab hbc := by cases a <;> cases b <;> cases c <;> simp_all
+
+instance : LawfulEqOrd HourMarker where
+  eq_of_compare {a b} h := by cases a <;> cases b <;> simp_all
 
 namespace HourMarker
 
diff --git a/src/Std/Time/Time/PlainTime.lean b/src/Std/Time/Time/PlainTime.lean
index cb299a60bd..46d0e9bd6d 100644
--- a/src/Std/Time/Time/PlainTime.lean
+++ b/src/Std/Time/Time/PlainTime.lean
@@ -15,6 +15,7 @@ set_option linter.all true
 /--
 Represents a specific point in a day, including hours, minutes, seconds, and nanoseconds.
 -/
+@[ext]
 structure PlainTime where
 
   /--
@@ -36,14 +37,30 @@ structure PlainTime where
   `Nanoseconds` component of the `PlainTime`
   -/
   nanosecond : Nanosecond.Ordinal
-  deriving Repr
+deriving Repr, DecidableEq
 
 instance : Inhabited PlainTime where
   default := ⟨0, 0, 0, 0, by decide⟩
 
-instance : BEq PlainTime where
-  beq x y := x.hour.val == y.hour.val && x.minute == y.minute
-          && x.second.val == y.second.val && x.nanosecond == y.nanosecond
+instance : Ord PlainTime where
+  compare := compareLex (compareOn (·.hour)) <| compareLex (compareOn (·.minute)) <|
+      compareLex (compareOn (·.second)) (compareOn (·.nanosecond))
+
+theorem PlainTime.compare_def :
+    compare (α := PlainTime) =
+      (compareLex (compareOn (·.hour)) <| compareLex (compareOn (·.minute)) <|
+          compareLex (compareOn (·.second)) (compareOn (·.nanosecond))) := rfl
+
+instance : TransOrd PlainTime := inferInstanceAs <| TransCmp (compareLex _ _)
+
+instance : LawfulEqOrd PlainTime where
+  eq_of_compare {a b} h := by
+    simp only [PlainTime.compare_def, compareLex_eq_eq] at h
+    ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2.1
+    · exact LawfulEqOrd.eq_of_compare h.2.2.1
+    · exact LawfulEqOrd.eq_of_compare h.2.2.2
 
 namespace PlainTime
 
diff --git a/src/Std/Time/Time/Unit/Hour.lean b/src/Std/Time/Time/Unit/Hour.lean
index fa200bb800..313e472e40 100644
--- a/src/Std/Time/Time/Unit/Hour.lean
+++ b/src/Std/Time/Time/Unit/Hour.lean
@@ -21,7 +21,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for hours, ranging from 0 to 23.
 -/
 def Ordinal := Bounded.LE 0 23
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
 
 instance : OfNat Ordinal n :=
   inferInstanceAs (OfNat (Bounded.LE 0 (0 + (23 : Nat))) n)
@@ -35,22 +35,34 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents an offset in hours, defined as an `Int`. This can be used to express durations
 or differences in hours.
 -/
 def Offset : Type := UnitVal 3600
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
 
-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 
+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Ordinal
 
 /--
diff --git a/src/Std/Time/Time/Unit/Millisecond.lean b/src/Std/Time/Time/Unit/Millisecond.lean
index 9452a51fac..e5e7365de8 100644
--- a/src/Std/Time/Time/Unit/Millisecond.lean
+++ b/src/Std/Time/Time/Unit/Millisecond.lean
@@ -20,7 +20,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for milliseconds, ranging from 0 to 999 milliseconds.
 -/
 def Ordinal := Bounded.LE 0 999
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
 
 instance : OfNat Ordinal n :=
   inferInstanceAs (OfNat (Bounded.LE 0 (0 + (999 : Nat))) n)
@@ -34,21 +34,33 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents a duration offset in milliseconds.
 -/
 def Offset : Type := UnitVal (1 / 1000)
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 
+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Offset
 
 /--
diff --git a/src/Std/Time/Time/Unit/Minute.lean b/src/Std/Time/Time/Unit/Minute.lean
index 14cddd68b9..5746391e12 100644
--- a/src/Std/Time/Time/Unit/Minute.lean
+++ b/src/Std/Time/Time/Unit/Minute.lean
@@ -20,7 +20,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for minutes, ranging from 0 to 59. This is useful for representing the minute component of a time.
 -/
 def Ordinal := Bounded.LE 0 59
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
 
 instance : OfNat Ordinal n :=
   inferInstanceAs (OfNat (Bounded.LE 0 (0 + (59 : Nat))) n)
@@ -34,21 +34,33 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents a duration offset in minutes.
 -/
 def Offset : Type := UnitVal 60
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
 
-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofInt <| Int.ofNat n⟩
 
+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Ordinal
 
 /--
diff --git a/src/Std/Time/Time/Unit/Nanosecond.lean b/src/Std/Time/Time/Unit/Nanosecond.lean
index 8e81975f2c..45dc277607 100644
--- a/src/Std/Time/Time/Unit/Nanosecond.lean
+++ b/src/Std/Time/Time/Unit/Nanosecond.lean
@@ -19,7 +19,7 @@ set_option linter.all true
 `Ordinal` represents a nanosecond value that is bounded between 0 and 999,999,999 nanoseconds.
 -/
 def Ordinal := Bounded.LE 0 999999999
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
 
 instance : OfNat Ordinal n where
   ofNat := Bounded.LE.ofFin (Fin.ofNat' _ n)
@@ -33,21 +33,33 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents a time offset in nanoseconds.
 -/
 def Offset : Type := UnitVal (1 / 1000000000)
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 
+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Offset
 
 /--
@@ -71,10 +83,22 @@ end Offset
 This can be used for operations that involve differences or adjustments within this range.
 -/
 def Span := Bounded.LE (-999999999) 999999999
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
 
 instance : Inhabited Span where default := Bounded.LE.mk 0 (by decide)
 
+instance {x y : Span} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Span} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
+instance : Ord Span := inferInstanceAs <| Ord (Bounded.LE _ _)
+
+instance : TransOrd Span := inferInstanceAs <| TransOrd (Bounded.LE _ _)
+
+instance : LawfulEqOrd Span := inferInstanceAs <| LawfulEqOrd (Bounded.LE _ _)
+
 namespace Span
 
 /--
@@ -91,7 +115,21 @@ namespace Ordinal
 `Ordinal` represents a bounded value for nanoseconds in a day, which ranges between 0 and 86400000000000.
 -/
 def OfDay := Bounded.LE 0 86400000000000
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
+
+instance : Inhabited OfDay where default := Bounded.LE.mk 0 (by decide)
+
+instance {x y : OfDay} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : OfDay} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
+instance : Ord OfDay := inferInstanceAs <| Ord (Bounded.LE _ _)
+
+instance : TransOrd OfDay := inferInstanceAs <| TransOrd (Bounded.LE _ _)
+
+instance : LawfulEqOrd OfDay := inferInstanceAs <| LawfulEqOrd (Bounded.LE _ _)
 
 /--
 Creates an `Ordinal` from an integer, ensuring the value is within bounds.
diff --git a/src/Std/Time/Time/Unit/Second.lean b/src/Std/Time/Time/Unit/Second.lean
index 1e3dd4f59f..dc8cbea39d 100644
--- a/src/Std/Time/Time/Unit/Second.lean
+++ b/src/Std/Time/Time/Unit/Second.lean
@@ -21,9 +21,6 @@ for potential leap second.
 -/
 def Ordinal (leap : Bool) := Bounded.LE 0 (.ofNat (if leap then 60 else 59))
 
-instance : BEq (Ordinal leap) where
-  beq x y := BEq.beq x.val y.val
-
 instance : LE (Ordinal leap) where
   le x y := LE.le x.val y.val
 
@@ -33,6 +30,9 @@ instance : LT (Ordinal leap) where
 instance : Repr (Ordinal leap) where
   reprPrec r := reprPrec r.val
 
+instance : ToString (Ordinal leap) where
+  toString r := toString r.val
+
 instance : OfNat (Ordinal leap) n := by
   have inst := inferInstanceAs (OfNat (Bounded.LE 0 (0 + (59 : Nat))) n)
   cases leap
@@ -45,21 +45,35 @@ instance {x y : Ordinal leap} : Decidable (x ≤ y) :=
 instance {x y : Ordinal leap} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
+instance : DecidableEq (Ordinal leap) := inferInstanceAs <| DecidableEq (Bounded.LE 0 _)
+
+instance : Ord (Ordinal leap) := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd (Ordinal leap) := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd (Ordinal leap) := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents an offset in seconds. It is defined as an `Int`.
 -/
 def Offset : Type := UnitVal 1
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
   inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 
+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Offset
 
 /--
diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean
index e016ba424d..6869e9dab5 100644
--- a/src/Std/Time/Zoned/DateTime.lean
+++ b/src/Std/Time/Zoned/DateTime.lean
@@ -33,8 +33,13 @@ structure DateTime (tz : TimeZone) where
 instance : BEq (DateTime tz) where
   beq x y := x.timestamp == y.timestamp
 
-instance : Inhabited (DateTime tz) where
-  default := ⟨Inhabited.default, Thunk.mk fun _ => Inhabited.default⟩
+instance : Ord (DateTime tz) where
+  compare := compareOn (·.timestamp)
+
+instance : TransOrd (DateTime tz) := inferInstanceAs <| TransCmp (compareOn _)
+
+instance : LawfulBEqOrd (DateTime tz) where
+  compare_eq_iff_beq := LawfulBEqOrd.compare_eq_iff_beq (α := Timestamp)
 
 namespace DateTime
 
@@ -45,6 +50,9 @@ Creates a new `DateTime` out of a `Timestamp` that is in a `TimeZone`.
 def ofTimestamp (tm : Timestamp) (tz : TimeZone) : DateTime tz :=
   DateTime.mk tm (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC |>.addSeconds tz.toSeconds)
 
+instance : Inhabited (DateTime tz) where
+  default := ofTimestamp Inhabited.default tz
+
 /--
 Converts a `DateTime` to the number of days since the UNIX epoch.
 -/
diff --git a/src/Std/Time/Zoned/Offset.lean b/src/Std/Time/Zoned/Offset.lean
index c6efccf550..a37e9059c6 100644
--- a/src/Std/Time/Zoned/Offset.lean
+++ b/src/Std/Time/Zoned/Offset.lean
@@ -16,6 +16,7 @@ set_option linter.all true
 /--
 Represents a timezone offset with an hour and second component.
 -/
+@[ext]
 structure Offset where
 
   /--
@@ -27,13 +28,24 @@ structure Offset where
   The same timezone offset in seconds.
   -/
   second : Second.Offset
-  deriving Repr
+deriving Repr, DecidableEq
 
 instance : Inhabited Offset where
   default := ⟨0⟩
 
-instance : BEq Offset where
-  beq x y := BEq.beq x.second y.second
+instance : Ord Offset where
+  compare := compareOn (·.second)
+
+theorem Offset.compare_def :
+    compare (α := Offset) = compareOn (·.second) := rfl
+
+instance : TransOrd Offset := inferInstanceAs <| TransCmp (compareOn _)
+
+instance : LawfulEqOrd Offset where
+  eq_of_compare {a b} h := by
+    simp only [Offset.compare_def] at h
+    apply Offset.ext
+    exact LawfulEqOrd.eq_of_compare h
 
 namespace Offset
 
diff --git a/src/Std/Time/Zoned/TimeZone.lean b/src/Std/Time/Zoned/TimeZone.lean
index 1dd0d6c3d8..6b4ec73fbd 100644
--- a/src/Std/Time/Zoned/TimeZone.lean
+++ b/src/Std/Time/Zoned/TimeZone.lean
@@ -36,7 +36,7 @@ structure TimeZone where
   Day light saving flag.
   -/
   isDST : Bool
-  deriving Inhabited, Repr, BEq
+deriving Inhabited, Repr, DecidableEq
 
 namespace TimeZone
 
diff --git a/tests/lean/run/dateTimeOrd.lean b/tests/lean/run/dateTimeOrd.lean
new file mode 100644
index 0000000000..bce1d3ebe8
--- /dev/null
+++ b/tests/lean/run/dateTimeOrd.lean
@@ -0,0 +1,48 @@
+import Std.Time
+
+open Std.Time
+
+def strictly_ordered {α} [Ord α] : List α → Bool
+  | [] => true
+  | [_] => true
+  | x :: y :: tail => compare x y = .lt && strictly_ordered (y :: tail)
+
+def plainDate1 := PlainDate.ofYearMonthDay? 2020 03 02 |>.get!
+def plainDate2 := PlainDate.ofYearMonthDay? 2025 01 02 |>.get!
+def plainDate3 := PlainDate.ofYearMonthDay? 2025 02 01 |>.get!
+
+example : Std.TransOrd PlainDate := inferInstance
+example : Std.LawfulEqOrd PlainDate := inferInstance
+example : Std.LawfulBEqOrd PlainDate := inferInstance
+example : strictly_ordered
+  [PlainDate.ofYearMonthDay? 2020 03 02 |>.get!,
+   PlainDate.ofYearMonthDay? 2025 01 02 |>.get!,
+   PlainDate.ofYearMonthDay? 2025 02 01 |>.get!] := by decide
+
+def plainTime1 := PlainTime.ofHourMinuteSecondsNano 0 0 0 1
+def plainTime2 := PlainTime.ofHourMinuteSecondsNano 0 0 1 0
+def plainTime3 := PlainTime.ofHourMinuteSecondsNano 0 1 0 0
+def plainTime4 := PlainTime.ofHourMinuteSecondsNano 1 0 0 0
+
+example : Std.TransOrd PlainTime := inferInstance
+example : Std.LawfulEqOrd PlainTime := inferInstance
+example : Std.LawfulBEqOrd PlainTime := inferInstance
+example : strictly_ordered
+  [PlainTime.ofHourMinuteSecondsNano 0 0 0 1,
+   PlainTime.ofHourMinuteSecondsNano 0 0 1 0,
+   PlainTime.ofHourMinuteSecondsNano 0 1 0 0,
+   PlainTime.ofHourMinuteSecondsNano 1 0 0 0] := by decide
+
+example : Std.TransOrd (DateTime TimeZone.GMT) := inferInstance
+example : Std.LawfulBEqOrd (DateTime TimeZone.GMT) := inferInstance
+
+-- We cannot use `decide` here because the reduction gets stuck.
+/-- info: true -/
+#guard_msgs in
+#eval strictly_ordered <|
+  ["Sat Jan 01 01:01:02 2025",
+   "Sat Jan 01 01:02:01 2025",
+   "Sat Jan 01 02:01:01 2025",
+   "Sat Jan 02 01:01:01 2025",
+   "Sat Feb 01 01:01:01 2025",
+   "Sat Jan 01 01:01:01 2026"].map (DateTime.fromAscTimeString . |>.toOption.get!)