```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  ```