import Algebra.Relation.Preorder

public export

public export

--
-- Order
--
data NaturalLTE : (x, y : Natural) -> Type where
  ZeroLTEAny : NaturalLTE Zero y
  SuccesorLTE : NaturalLTE x y -> NaturalLTE (Succesor x) (Succesor y)
public export
Uninhabited (NaturalLTE (Succesor y) Zero) where
  uninhabited ZeroLTEAny impossible
  uninhabited (SuccesorLTE _) impossible
public export
proofNotLTEThenNotSuccesorLTE : Not (NaturalLTE x y) -> Not (NaturalLTE (Succesor x) (Succesor y))
proofNotLTEThenNotSuccesorLTE h (SuccesorLTE ctra) = h ctra
public export
Preorder Natural where
  LTE = NaturalLTE
  decLTE Zero y = Yes ZeroLTEAny
  decLTE (Succesor _) Zero = No absurd
  decLTE (Succesor x) (Succesor y) =
    case decLTE x y of
      Yes p => Yes $ SuccesorLTE p
      No cp => No $ proofNotLTEThenNotSuccesorLTE cp
  proofReflexivity Zero = ZeroLTEAny
  proofReflexivity (Succesor x) = SuccesorLTE $ proofReflexivity x
  proofTransitivity Zero        Zero            z  ZeroLTEAny  ZeroLTEAny     = ZeroLTEAny
  proofTransitivity Zero (Succesor y) (Succesor z) ZeroLTEAny (SuccesorLTE p) = ZeroLTEAny
  proofTransitivity (Succesor x) (Succesor y) (Succesor z) (SuccesorLTE p1) (SuccesorLTE p2) =
    SuccesorLTE $ proofTransitivity x y z p1 p2