{-# OPTIONS --safe #-}

module Data.Nat.Order where

open import Prelude
open import Agda.Builtin.Nat
  renaming (_<_ to infix 4 _<ᴮ_)
  public

-- _<_ : Nat → Nat → Bool
-- _     < zero  = false
-- zero  < suc _ = true
-- suc n < suc m = n < m

_⊔_ _⊔suc_ : ℕ → ℕ → ℕ
zero  ⊔ y = y
suc x ⊔ y = suc (y ⊔suc x)
zero  ⊔suc x = x
suc y ⊔suc x = x ⊔ y

infix 4 _≤ᴮ_ _≤_ _<_

_≤ᴮ_ : ℕ → ℕ → Bool
n ≤ᴮ m = n <ᴮ suc m

_≤_ _<_ : ℕ → ℕ → Type
n ≤ m = T (n ≤ᴮ m)
n < m = T (n <ᴮ m)

≤-⊔ˡ : ∀ x y z → x ≤ y → x ≤ y ⊔ z
≤-⊔ˡ zero y z x≤y = tt
≤-⊔ˡ (suc x) (suc y) zero x≤y = x≤y
≤-⊔ˡ (suc x) (suc y) (suc z) x≤y = ≤-⊔ˡ x y z x≤y

≤-⊔ʳ : ∀ x z y → x ≤ y → x ≤ z ⊔ y
≤-⊔ʳ zero    y z x≤y = tt
≤-⊔ʳ (suc x) zero (suc z) x≤y = x≤y
≤-⊔ʳ (suc x) (suc y) (suc z) x≤y = ≤-⊔ʳ x y z x≤y

≤-refl : ∀ n → n ≤ n
≤-refl zero = tt
≤-refl (suc n) = ≤-refl n

<-irrefl : ∀ n → ¬ (n < n)
<-irrefl (suc n) n<n = <-irrefl n n<n

≤-sucʳ : ∀ n m → n ≤ m → n ≤ suc m
≤-sucʳ zero zero n≤m = tt
≤-sucʳ zero (suc m) n≤m = tt
≤-sucʳ (suc n) (suc m) n≤m = ≤-sucʳ n m n≤m