{-# 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