import Algebra.Relation.Order

public export
proofLTEThenLTESuccesor : NaturalLTE x y -> NaturalLTE x (Succesor y)
proofLTEThenLTESuccesor {x=Zero} ZeroLTEAny = ZeroLTEAny
proofLTEThenLTESuccesor (SuccesorLTE p) = SuccesorLTE $ proofLTEThenLTESuccesor p

public export
Order Natural where
  LT x = NaturalLTE (Succesor x)
  decLT Zero Zero = No absurd
  decLT Zero (Succesor y) = Yes $ SuccesorLTE ZeroLTEAny
  decLT (Succesor _) Zero = No absurd
  decLT (Succesor x) (Succesor y) =
     case decLT x y of
       Yes p => Yes $ SuccesorLTE p
       No cp => No $ proofNotLTEThenNotSuccesorLTE cp
  proofAntisymetry Zero Zero ZeroLTEAny ZeroLTEAny = BothZero
  proofAntisymetry (Succesor x) (Succesor y) (SuccesorLTE p1) (SuccesorLTE p2) =
    SuccesorEquiv $ proofAntisymetry x y p1 p2
  proofLTThenLTE (SuccesorLTE p) = proofLTEThenLTESuccesor p
  proofLTEThenLTOrEquiv Zero Zero ZeroLTEAny = Right BothZero
  proofLTEThenLTOrEquiv Zero (Succesor y) ZeroLTEAny = Left $ SuccesorLTE ZeroLTEAny
  proofLTEThenLTOrEquiv (Succesor x) (Succesor y) (SuccesorLTE p) =
    case proofLTEThenLTOrEquiv x y p of
      Left l => Left $ SuccesorLTE l
      Right e => Right $ SuccesorEquiv e

import Data.Either

import public Data.Either