module ordering where

{-
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
-}

open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥)
open import Relation.Nullary using (¬_)
open import Data.Sum using (_⊎_; inj₁; inj₂)

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

2≤4 : 2 ≤ 4
2≤4 = {!!}

¬4≤2 : ¬ (4 ≤ 2)
¬4≤2 = {!!}

≤-refl : ∀ {n : ℕ} → n ≤ n
≤-refl = {!!}

≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans = {!!}

≤-trans′ : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans′ = {!!}

≤-total : ∀ (m n : ℕ) → (m ≤ n) ⊎ (n ≤ m)
≤-total = {!!}

-- < defined using ≤
_<_ : ℕ → ℕ → Set
m < n = suc m ≤ n

data Dec (P : Set) : Set where
  yes : P   → Dec P
  no  : ¬ P → Dec P

¬s≤z : ∀ (n : ℕ) → ¬ (suc n ≤ zero)
¬s≤z = {!!}

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s = {!!}

≤? : ∀ (m n : ℕ) → Dec (m ≤ n)
≤? = {!!}