Add structures/bundles for pairs of strict and non-strict orders

[MatthewDaggitt]

Currently, whenever we have a generic proof that involves both a non-strict and a strict order we translate from one to the other using Relation.Binary.Construct.NonStrictToStrict/StrictToNonStrict. This works fine for generic data, but runs into serious problems when dealing with data where the non-strict and strict orders exploit some structure of the data and are therefore not defined in that way. The most common examples are our numeric datatypes.

Currently we've been getting around this by adding specialised modules for each of the numeric datatypes, e.g. Data.List.Extrema.Nat, but this doesn't scale very well as it requires a module for each problematic datatype.

I propose adding some additional relational structures/bundles to the library along the following lines (names are definitely open for discussion!):

record IsStrictNonStrictPair (_≤_ : Rel A ℓ₂) (_<_ : Rel A ℓ₃) : Set (a ⊔ ℓ ⊔ ℓ₂ ⊔ ℓ₃) where
   field
    <⇒≉    : _<_ ⇒ _≉_
    <⇒≤    : _<_ ⇒ _≤_
    ≤∧≉⇒<  : ∀ {x y} → x ≤ y → x ≉ y → x < y

record IsTotalOrderPair (_≤_ : Rel A ℓ₂) (_<_ : Rel A ℓ₃) : Set (a ⊔ ℓ ⊔ ℓ₂ ⊔ ℓ₃) where
  field
    isTotalOrder          : IsTotalOrder _≤_
    isStrictTotalOrder    : IsStrictTotalOrder _<_
    isStrictNonStrictPair : IsStrictNonStrictPair _≤_ _<_

This would then allow us to prove these properties once, rather than having a specialisation for each datatype.

[gallais]

Is _≉_ from a setoid? So it's more like a triple than a pair then.