自然數上的標準序#

≤-refl : {a : ℕ} → a ≤ a
≤-refl {zero}   = z≤n
≤-refl {succ a} = s≤s ≤-refl

≤-trans : {a b c : ℕ} → a ≤ b → b ≤ c → a ≤ c
≤-trans z≤n     q       = z≤n
≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q)

≤-antisymm : {a b : ℕ} → a ≤ b → b ≤ a → a ≡ b
≤-antisymm z≤n     z≤n     = refl
≤-antisymm (s≤s p) (s≤s q) = cong succ (≤-antisymm p q)

<-irreflexive : {a : ℕ} → a < a → ⊥
<-irreflexive (s≤s p) = <-irreflexive p

<-irreflexive' : {a b : ℕ} → a ≤ b → b < a → ⊥
<-irreflexive' (s≤s p) (s≤s q) = <-irreflexive' p q

<-irreflexive'' : {a b : ℕ} → a < b → b < a → ⊥
<-irreflexive'' (s≤s p) (s≤s q) = <-irreflexive'' p q

≡⇒≤ : {a b : ℕ} → a ≡ b → a ≤ b
≡⇒≤ refl = ≤-refl

≤-<-connex : (a b : ℕ) → a ≤ b ⊎ b < a
≤-<-connex zero     b        = left z≤n
≤-<-connex (succ a) zero     = right (s≤s z≤n)
≤-<-connex (succ a) (succ b) with ≤-<-connex a b
... | left  a≤b = left  (s≤s a≤b)
... | right b<a = right (s≤s b<a)

<-cmp : (a b : ℕ) → a ≡ b ⊎ (a < b ⊎ a > b)
<-cmp zero     zero     = left refl
<-cmp zero     (succ b) = right (left (s≤s z≤n))
<-cmp (succ a) zero     = right (right (s≤s z≤n))
<-cmp (succ a) (succ b) with <-cmp a b
... | left  a≡b         = left (cong succ a≡b)
... | right (left a<b)  = right (left (s≤s a<b))
... | right (right a>b) = right (right (s≤s a>b))

dec-≤ : (a b : ℕ) → Dec (a ≤ b)
dec-≤ zero     b = yes z≤n
dec-≤ (succ a) zero = no λ ()
dec-≤ (succ a) (succ b) with dec-≤ a b
... | yes a≤b  = yes (s≤s a≤b)
... | no  ¬a≤b = no λ { (s≤s a≤b) → ¬a≤b a≤b }

dec-< : (a b : ℕ) → Dec (a < b)
dec-< a b = dec-≤ (succ a) b

pred-monotone : {a b : ℕ} → a ≤ b → pred a ≤ pred b
pred-monotone z≤n     = z≤n
pred-monotone (s≤s p) = p

succ-inflationary : (a : ℕ) → a ≤ succ a
succ-inflationary zero     = z≤n
succ-inflationary (succ a) = s≤s (succ-inflationary a)

twice-inflationary : (a : ℕ) → a ≤ twice a
twice-inflationary zero     = z≤n
twice-inflationary (succ a) = ≤-trans (succ-inflationary (succ a)) (succ-monotone (succ-monotone (twice-inflationary a)))

max-inflationaryₗ : (a b : ℕ) → a ≤ max a b
max-inflationaryₗ zero     b        = z≤n
max-inflationaryₗ (succ a) zero     = ≤-refl
max-inflationaryₗ (succ a) (succ b) = s≤s (max-inflationaryₗ a b)

max-inflationaryᵣ : (a b : ℕ) → b ≤ max a b
max-inflationaryᵣ zero     b        = ≤-refl
max-inflationaryᵣ (succ a) zero     = z≤n
max-inflationaryᵣ (succ a) (succ b) = s≤s (max-inflationaryᵣ a b)

+-monotone : {a a' b b' : ℕ} → a ≤ b → a' ≤ b' → a + a' ≤ b + b'
+-monotone z≤n     z≤n     = z≤n
+-monotone z≤n     (s≤s q) = ≤-trans (succ-monotone (+-monotone z≤n q)) (≡⇒≤ (sym (+-succ _ _)))
+-monotone (s≤s p) q       = succ-monotone (+-monotone p q)

+-inflationaryₗ : (a b : ℕ) → a ≤ a + b
+-inflationaryₗ zero     b = z≤n
+-inflationaryₗ (succ a) b = s≤s (+-inflationaryₗ a b)

+-inflationaryᵣ : (a b : ℕ) → b ≤ a + b
+-inflationaryᵣ a b = +-monotone {zero} {b} {a} {b} z≤n ≤-refl

half-≤ : (x : ℕ) → half x ≤ x
half-≤ zero            = z≤n
half-≤ (succ zero)     = z≤n
half-≤ (succ (succ x)) = succ-monotone (≤-trans (half-≤ x) (succ-inflationary x))

half-< : (x : ℕ) → half (succ x) < succ x
half-< zero     = s≤s z≤n
half-< (succ x) = succ-monotone (succ-monotone (half-≤ x))

monus-≤ : (a b : ℕ) → a ≥ b → a ∸ b ≤ a
monus-≤ a        zero     z≤n       = ≤-refl
monus-≤ (succ a) (succ b) (s≤s a≥b) = ≤-trans (monus-≤ a b a≥b) (succ-inflationary a)

monus-< : (a b : ℕ) → IsPositive b → a ≥ b → a ∸ b < a
monus-< (succ a) (succ zero)     b≥0  (s≤s a≥b) = ≤-refl
monus-< (succ a) (succ (succ b)) b≥-1 (s≤s a>b) =
  ≤-trans (monus-< a (succ b) (case-succ b) a>b) (succ-inflationary a)

Even-infinite : (x : ℕ) → ∃[ y ] (y ≥ x × Even y)
Even-infinite x = twice x , twice-inflationary x , twice-even x
-- 或者，更經濟地，改以 `x` 或 `succ x` 作為見證，
-- 而不是 `twice x`：
-- Even-infinite x with even-or-odd x
-- ... | left  xeven = x      , ≤-refl              , xeven
-- ... | right xodd  = succ x , succ-inflationary x , succ-odd xodd

ℕ-infinite : (xs : List ℕ) → ∃[ x ] x ∉ xs
ℕ-infinite xs = succ (sum xs) , λ p → <-irreflexive (go p)
  where
  go : {xs : List ℕ} {y : ℕ} → y ∈ xs → y < succ (sum xs)
  go (here  refl) = succ-monotone (≤-trans (≡⇒≤ (sym (+-zero _))) (+-monotone ≤-refl z≤n))
  go (there p)    = ≤-trans (go p) (succ-monotone (+-monotone z≤n ≤-refl))

z<'s : {x : ℕ} → zero <' succ x
z<'s {zero}   = base'
z<'s {succ x} = step' z<'s

s<'s : {x y : ℕ} → x <' y → succ x <' succ y
s<'s base'     = base'
s<'s (step' p) = step' (s<'s p)

<⇒<' : {x y : ℕ} → x < y → x <' y
<⇒<' (s≤s p) = lemma p
  where
  lemma : {x y : ℕ} → x ≤ y → x <' succ y
  lemma z≤n     = z<'s
  lemma (s≤s p) = s<'s (lemma p)

<'⇒< : {x y : ℕ} → x <' y → x < y
<'⇒< base'     = ≤-refl
<'⇒< (step' p) = ≤-trans (<'⇒< p) (succ-inflationary _)

lookup : {P : ℕ → Set} {n m : ℕ} → All P (downFrom n) → m < n → P m
lookup {P} {succ n} {m} (p ∷ ps) m<n with ≤-<-connex n m
... | left  n≤m = subst P (≤-antisymm n≤m (pred-monotone m<n)) p
... | right m<n = lookup ps m<n