diff --git a/Class/HasOrder/Core.agda b/Class/HasOrder/Core.agda
index 8a2c056..35379b9 100644
--- a/Class/HasOrder/Core.agda
+++ b/Class/HasOrder/Core.agda
@@ -85,20 +85,53 @@ module _ {a} {A : Set a} where
       <⇒¬>⊎≈ x<y (inj₁ y<x) = <-asymmetric x<y y<x
       <⇒¬>⊎≈ x<y (inj₂ x≈y) = <-irrefl (≈-sym x≈y) x<y
 
+      ≥⇒≮ : ∀ {x y} → y ≤ x → ¬ (x < y)
+      ≥⇒≮ y≤x x<y = contradiction (to ≤⇔<∨≈ y≤x) (<⇒¬>⊎≈ x<y)
+
+    open HasPartialOrder ⦃...⦄
+
     record HasDecPartialOrder : Set (suc a) where
       field
         ⦃ hasPartialOrder ⦄ : HasPartialOrder
         ⦃ dec-≤ ⦄ : _≤_ ⁇²
         ⦃ dec-< ⦄ : _<_ ⁇²
 
+    record HasTotalOrder : Set (suc a) where
+      field
+        ⦃ hasPartialOrder ⦄ : HasPartialOrder
+        ≤-total : Total _≤_
+
+      ≤-isTotalOrder : IsTotalOrder _≈_ _≤_
+      ≤-isTotalOrder = record { isPartialOrder = ≤-isPartialOrder ; total = ≤-total }
+
+      open IsEquivalence ≈-isEquivalence renaming (sym to ≈-sym)
+
+      ≮⇒≥ : Decidable _≈_ → ∀ {x y} → ¬ (x < y) → y ≤ x
+      ≮⇒≥ _≈?_ {x} {y} x≮y with x ≈? y | ≤-total y x
+      ... | yes x≈y  | _        = IsPreorder.reflexive ≤-isPreorder (≈-sym x≈y)
+      ... | _        | inj₁ y≤x = y≤x
+      ... | no  x≉y  | inj₂ x≤y = contradiction (≤∧≉⇒< (x≤y , x≉y)) x≮y
+
+    open HasTotalOrder ⦃...⦄
+
+    record HasDecTotalOrder : Set (suc a) where
+      field
+        ⦃ hasTotalOrder ⦄ : HasTotalOrder
+        ⦃ dec-≤ ⦄ : _≤_ ⁇²
+        ⦃ dec-< ⦄ : _<_ ⁇²
+
   HasPreorder≡        = HasPreorder {_≈_ = _≡_}
   HasDecPreorder≡     = HasDecPreorder {_≈_ = _≡_}
   HasPartialOrder≡    = HasPartialOrder {_≈_ = _≡_}
   HasDecPartialOrder≡ = HasDecPartialOrder {_≈_ = _≡_}
+  HasTotalOrder≡      = HasTotalOrder {_≈_ = _≡_}
+  HasDecTotalOrder≡   = HasDecTotalOrder {_≈_ = _≡_}
 
 open HasPreorder ⦃...⦄ public
 open HasPartialOrder ⦃...⦄ public hiding (hasPreorder)
 open HasDecPartialOrder ⦃...⦄ public hiding (hasPartialOrder)
+open HasTotalOrder ⦃...⦄ public hiding (hasPartialOrder)
+open HasDecTotalOrder ⦃...⦄ public hiding (hasTotalOrder)
 
 module _ {a} {A : Set a} {_≈_ : Rel A a} where
 
diff --git a/Class/HasOrder/Instance.agda b/Class/HasOrder/Instance.agda
index 9c21070..afa9c13 100644
--- a/Class/HasOrder/Instance.agda
+++ b/Class/HasOrder/Instance.agda
@@ -20,6 +20,9 @@ instance
   ℕ-hasPartialOrder = HasPartialOrder ∋ record
     { ≤-antisym = Nat.≤-antisym }
   ℕ-hasDecPartialOrder = HasDecPartialOrder {A = ℕ} ∋ record {}
+  ℕ-hasTotalOrder = HasTotalOrder ∋ record
+    { ≤-total = Nat.≤-total }
+  ℕ-hasDecTotalOrder = HasDecTotalOrder {A = ℕ} ∋ record {}
 
   import Data.Integer.Properties as Int hiding (_≟_)
   ℤ-hasPreorder = HasPreorder ∋ record {Int; ≤⇔<∨≈ = let open Int in mk⇔
@@ -27,9 +30,15 @@ instance
     [ <⇒≤ , ≤-reflexive ] }
   ℤ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Int.≤-antisym }
   ℤ-hasDecPartialOrder = HasDecPartialOrder {A = ℤ} ∋ record {}
+  ℤ-hasTotalOrder = HasTotalOrder ∋ record
+    { ≤-total = Int.≤-total }
+  ℤ-hasDecTotalOrder = HasDecTotalOrder {A = ℤ} ∋ record {}
 
   import Data.Rational.Properties as Rat hiding (_≟_)
 
   ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
   ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
   ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}
+  ℚ-hasTotalOrder = HasTotalOrder ∋ record
+    { ≤-total = Rat.≤-total }
+  ℚ-hasDecTotalOrder = HasDecTotalOrder {A = ℚ} ∋ record {}