Additional data types related to ordering notions

`data Trichotomous : (a -> a -> Type) -> (a -> a -> Type) -> (a -> a -> Type) -> a -> a -> Type`

Trichotomous formalises the fact that three relations are mutually exclusive.

It is meant to be used with relations that complement each other so that the

`Trichotomous lt eq gt` relation is the total relation.

**Totality**: total

**Visibility**: public export

**Constructors**:`MkLT : lt v w -> Not (eq v w) -> Not (gt v w) -> Trichotomous lt eq gt v w`

`MkEQ : Not (lt v w) -> eq v w -> Not (gt v w) -> Trichotomous lt eq gt v w`

`MkGT : Not (lt v w) -> Not (eq v w) -> gt v w -> Trichotomous lt eq gt v w`