```{-# OPTIONS --type-in-type
#-}

open import NeilPrelude

module StrictPreOrder {A : Set} (_<'_ : Rel A)

(irreflex : Irreflexive _<'_)
(transit  : Transitive _<'_)

where

------------------------------------------------------------------

infix 3 _>_ _<_

_<_ : Rel A
_<_ = _<'_

_>_ : Rel A
a > b = b < a

irreflexive : Irreflexive _<_
irreflexive = irreflex

<-trans : Transitive _<_
<-trans = transit

------------------------------------------------------------------

lem-less→Neq : {a b : A} → (a < b) → a ≢ b
lem-less→Neq p refl = irreflex p

lem-more→Neq : {a b : A} → (a > b) → a ≢ b
lem-more→Neq p refl = irreflex p

------------------------------------------------------------------

_≤_ : Rel A
a ≤ b = (a < b) ⊎ a ≡ b

_≥_ : Rel A
a ≥ b = b ≤ a

------------------------------------------------------------------

reflexive : Reflexive _≤_
reflexive = inr refl

≤-refl : Reflexive _≤_
≤-refl = reflexive

≤-trans : Transitive _≤_
≤-trans (inl p) (inl q) = inl (<-trans p q)
≤-trans p (inr refl)    = p
≤-trans (inr refl) q    = q

------------------------------------------------------------------

<≤-trans : Trans _<_ _≤_ _<_
<≤-trans p (inl q)    = <-trans p q
<≤-trans p (inr refl) = p

≤<-trans : Trans _≤_ _<_ _<_
≤<-trans (inl p) q    = <-trans p q
≤<-trans (inr refl) q = q

------------------------------------------------------------------
```