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

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

    open import Relation.Binary.Bundles using (TotalOrder; DecTotalOrder)

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

    open import Data.Product.Base using (proj₁)
    open import Data.Sum.Base using (inj₁; inj₂)
    import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
    open import Relation.Binary.Definitions using (Decidable)
    open import Relation.Binary.Structures using (IsTotalOrder)
    open import Relation.Binary.Consequences using (total∧dec⇒dec)

    open TotalOrder T

    import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
    import Relation.Binary.Properties.Poset poset as PosetProperties

    ------------------------------------------------------------------------
    -- 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 = EqAndOrd.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)