module Nat where

-- Re-export everything from Data.Nat except _≤_ and _≥_
open import Data.Nat public hiding (_≤_; _≥_)
open import Data.Bool

_≤_ :     Bool
zero   n     = true
suc m  zero  = false
suc m  suc n = m  n

_≥_ :     Bool
m  n = n  m