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