```------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by total orders
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary

module Relation.Binary.Properties.TotalOrder
{t₁ t₂ t₃} (T : TotalOrder t₁ t₂ t₃) where

open TotalOrder T

open import Data.Product using (proj₁)
open import Data.Sum.Base using (inj₁; inj₂)
import Relation.Binary.Construct.Converse as Converse
import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
import Relation.Binary.Properties.Poset poset as PosetProperties
open import Relation.Binary.Consequences
open import Relation.Nullary.Negation using (¬_)

------------------------------------------------------------------------
-- Total orders are almost decidable total orders

decTotalOrder : Decidable _≈_ → DecTotalOrder _ _ _
decTotalOrder ≟ = record
{ isDecTotalOrder = record
{ isTotalOrder = isTotalOrder
; _≟_          = ≟
; _≤?_         = total∧dec⇒dec reflexive antisym total ≟
}
}

------------------------------------------------------------------------
-- _≥_ - the flipped relation is also a total order

open PosetProperties public
using
( _≥_
; ≥-refl
; ≥-reflexive
; ≥-trans
; ≥-antisym
; ≥-isPreorder
; ≥-isPartialOrder
; ≥-preorder
; ≥-poset
)

≥-isTotalOrder : IsTotalOrder _≈_ _≥_
≥-isTotalOrder = Converse.isTotalOrder isTotalOrder

≥-totalOrder : TotalOrder _ _ _
≥-totalOrder = record
{ isTotalOrder = ≥-isTotalOrder
}

open TotalOrder ≥-totalOrder public
using () renaming (total to ≥-total)

------------------------------------------------------------------------
-- _<_ - the strict version is a strict partial order

-- Note that total orders can NOT be turned into strict total orders as
-- in order to distinguish between the _≤_ and _<_ cases we must have
-- decidable equality _≈_.

open PosetProperties public
using
( _<_
; <-resp-≈
; <-respʳ-≈
; <-respˡ-≈
; <-irrefl
; <-asym
; <-trans
; <-isStrictPartialOrder
; <-strictPartialOrder
; <⇒≉
; ≤∧≉⇒<
; <⇒≱
; ≤⇒≯
)

------------------------------------------------------------------------
-- _≰_ - the negated order

open PosetProperties public
using
( _≰_
; ≰-respʳ-≈
; ≰-respˡ-≈
)

≰⇒> : ∀ {x y} → x ≰ y → y < x
≰⇒> = ToStrict.≰⇒> Eq.sym reflexive total

≰⇒≥ : ∀ {x y} → x ≰ y → y ≤ x
≰⇒≥ x≰y = proj₁ (≰⇒> x≰y)
```