Idris2Doc : Decidable.Order.Strict

Decidable.Order.Strict

```An strict preorder (sometimes known as a quasi-order, or an
ordering) is what you get when you remove the diagonal `{(a,b) | a
r b , b r a}` from a preorder. For example a < b is an ordering.
This module extends base's Control.Order with the strict versions.
The interface system seems to struggle a bit with some of the constructions,
so I hacked them a bit. Sorry.
```

Definitions

`interface Irreflexive : (ty : Type) -> (ty -> ty -> Type) -> Type`
Parameters: ty, rel
Methods:
`irreflexive : Not (rel x x)`

Implementation:
`Irreflexive Nat LT`
`irreflexive : Irreflexive ty rel => Not (rel x x)`
Totality: total
Visibility: public export
`interface StrictPreorder : (ty : Type) -> (ty -> ty -> Type) -> Type`
Parameters: ty, rel
Constraints: Transitive ty rel, Irreflexive ty rel
Implementation:
`StrictPreorder Nat LT`
`interface Asymmetric : (ty : Type) -> (ty -> ty -> Type) -> Type`
Parameters: ty, rel
Methods:
`asymmetric : rel x y -> Not (rel y x)`
`asymmetric : Asymmetric ty rel => rel x y -> Not (rel y x)`
Totality: total
Visibility: public export
`record EqOr : Rel t -> t -> t -> Type`
Totality: total
Visibility: public export
Constructor:
`MkEqOr : Either (a = b) (spo a b) -> EqOr spo a b`

Projection:
`.runEqOr : EqOr spo a b -> Either (a = b) (spo a b)`

Hints:
`(Irreflexive ty rel, Asymmetric ty rel) => Antisymmetric ty (EqOr rel)`
`Connex ty rel => Connex ty (EqOr rel)`
`(Irreflexive ty rel, (Asymmetric ty rel, Transitive ty rel)) => PartialOrder ty (EqOr rel)`
`Transitive ty rel => Preorder ty (EqOr rel)`
`Reflexive ty (EqOr rel)`
`(Connex ty rel, DecEq ty) => StronglyConnex ty (EqOr rel)`
`Transitive ty rel => Transitive ty (EqOr rel)`
`.runEqOr : EqOr spo a b -> Either (a = b) (spo a b)`
Totality: total
Visibility: public export
`runEqOr : EqOr spo a b -> Either (a = b) (spo a b)`
Totality: total
Visibility: public export
`data DecOrdering : t -> t -> Type`
Totality: total
Visibility: public export
Constructors:
`DecLT : lt a b -> DecOrdering a b`
`DecEQ : a = b -> DecOrdering a b`
`DecGT : lt b a -> DecOrdering a b`
`interface StrictOrdered : (t : Type) -> (t -> t -> Type) -> Type`
Parameters: t, spo
Constraints: StrictPreorder t spo
Methods:
`order : (a : t) -> (b : t) -> DecOrdering a b`

Implementation:
`StrictOrdered Nat LT`
`order : StrictOrdered t spo => (a : t) -> (b : t) -> DecOrdering a b`
Totality: total
Visibility: public export