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

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

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

    module Relation.Binary.Properties.DecTotalOrder
      {d₁ d₂ d₃} (DTO : DecTotalOrder d₁ d₂ d₃) where

    import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
      using (isDecTotalOrder)
    open import Relation.Binary.Structures
      using (IsDecTotalOrder; IsStrictTotalOrder)
    open import Relation.Nullary.Negation.Core using (¬_)

    open DecTotalOrder DTO hiding (trans)

    import Relation.Binary.Properties.TotalOrder totalOrder as TotalOrderProperties
    import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict

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

    open TotalOrderProperties public
      using
      ( ≥-refl
      ; ≥-reflexive
      ; ≥-trans
      ; ≥-antisym
      ; ≥-total
      ; ≥-isPreorder
      ; ≥-isPartialOrder
      ; ≥-isTotalOrder
      ; ≥-preorder
      ; ≥-poset
      ; ≥-totalOrder
      )

    ≥-isDecTotalOrder : IsDecTotalOrder _≈_ _≥_
    ≥-isDecTotalOrder = EqAndOrd.isDecTotalOrder isDecTotalOrder

    ≥-decTotalOrder : DecTotalOrder _ _ _
    ≥-decTotalOrder = record
      { isDecTotalOrder = ≥-isDecTotalOrder
      }

    open DecTotalOrder ≥-decTotalOrder public
      using () renaming (_≤?_ to _≥?_)

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

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

    <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
    <-isStrictTotalOrder = ToStrict.<-isStrictTotalOrder₂ isDecTotalOrder

    <-strictTotalOrder : StrictTotalOrder _ _ _
    <-strictTotalOrder = record
      { isStrictTotalOrder = <-isStrictTotalOrder
      }

    open StrictTotalOrder <-strictTotalOrder public
      using (_≮_) renaming (compare to <-compare)

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

    open TotalOrderProperties public
      using
      ( ≰-respʳ-≈
      ; ≰-respˡ-≈
      ; ≰⇒>
      ; ≰⇒≥
      )

    ≮⇒≥ : ∀ {x y} → x ≮ y → y ≤ x
    ≮⇒≥ = ToStrict.≮⇒≥ Eq.sym _≟_ reflexive total