module MiniLibrary.Nat where

open import MiniLibrary.Base

data   : Set where
 zero :  
 suc :   ->  

{-# BUILTIN NATURAL     #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

infix 4 _<ℕb_ _<ℕ_ _≤ℕb_ _≤ℕ_ _==ℕb_ _==ℕ_ _≥ℕb_ _≥ℕ_
infixl 6 _+_
infixl 7 _*_

_<ℕb_ :   ->   -> Bool
_   <ℕb  zero     = false
zero   <ℕb  _     = true
suc n <ℕb  suc m = n <ℕb  m


_<ℕ_ :     Set
n <ℕ m = True (n <ℕb m)


_≤ℕb_ :   ->   -> Bool
zero   ≤ℕb  _     = true
_   ≤ℕb  zero   = false
suc n ≤ℕb  suc m = n ≤ℕb  m



_≤ℕ_ :     Set
n ≤ℕ m = True (n ≤ℕb m)

_≥ℕb_ :   ->   -> Bool
n ≥ℕb m = m ≤ℕb n


_≥ℕ_ :   ->   -> Set
n ≥ℕ m = m ≤ℕ n


_==ℕb_ :   ->   -> Bool
zero   ==ℕb  zero     = true
zero   ==ℕb  suc _   = false
suc _ ==ℕb  zero     = false
suc n ==ℕb  suc m   = n ==ℕb  m

_==ℕ_ :     Set
n ==ℕ m = True (n ==ℕb m)


decideℕ : (n m : )  n <ℕ   m  n ==ℕ  m  m <ℕ  n
decideℕ zero     zero     = in1 triv
decideℕ zero     (suc m) = in0 triv
decideℕ (suc n) zero     = in2 triv
decideℕ (suc n) (suc m) = decideℕ n m


decideℕ≤   : (n m : )  n ≤ℕ m    m ≤ℕ  n
decideℕ≤ zero     _       = inl triv
decideℕ≤ _        zero    = inr triv
decideℕ≤ (suc n) (suc m) = decideℕ≤ n m


_+_ :      
n + zero = n
n + (suc m) = suc (n  + m)
{-# BUILTIN NATPLUS _+_ #-}


_∸_  :      
zero  _    = zero
n     zero = n
suc n  suc m = n  m

_*_ :      
n * zero = zero
n * (suc m) = n * m + n


pred :   
pred zero    = zero
pred (suc n) = n


==impliesℕ≤   : (n m : )  (n ==ℕ   m)  n ≤ℕ  m
==impliesℕ≤  zero     zero      p  = triv
==impliesℕ≤  zero     (suc m)   () 
==impliesℕ≤  (suc n)  zero      () 
==impliesℕ≤  (suc n)  (suc m)   p = ==impliesℕ≤  n  m   p