Chuangjie Xu, 2013

\begin{code}

module Inequality where

open import MiniLibrary


infix 30 _≤_
infix 30 _<_
infix 30 _≰_
infix 30 _≮_

data _≤_ : ℕ → ℕ → Set where
 ≤-zero : ∀{n : ℕ} → 0 ≤ n
 ≤-succ : ∀{m n : ℕ} → m ≤ n → succ m ≤ succ n

_<_ : ℕ → ℕ → Set
m < n = succ m ≤ n

_≰_ : ℕ → ℕ → Set
m ≰ n = ¬ (m ≤ n)

_≮_ : ℕ → ℕ → Set
m ≮ n = ¬ (m < n)

≤-pred : {n m : ℕ} → succ n ≤ succ m → n ≤ m
≤-pred (≤-succ r) = r

Lemma[a≤b-decidable] : ∀{a b : ℕ} → decidable (a ≤ b)
Lemma[a≤b-decidable] {0}      {0}      = in₀ ≤-zero
Lemma[a≤b-decidable] {0}      {succ b} = in₀ ≤-zero
Lemma[a≤b-decidable] {succ a} {0}      = in₁ (λ ())
Lemma[a≤b-decidable] {succ a} {succ b} = cases c₀ c₁ IH
 where
  IH : decidable (a ≤ b)
  IH = Lemma[a≤b-decidable] {a} {b}
  c₀ : a ≤ b → succ a ≤ succ b
  c₀ r = ≤-succ r
  c₁ : ¬ (a ≤ b) → ¬ (succ a ≤ succ b)
  c₁ f sr = ∅-elim (f (≤-pred sr))

Lemma[a≤b≤c→a≤c] : ∀{a b c : ℕ} → a ≤ b → b ≤ c → a ≤ c
Lemma[a≤b≤c→a≤c] ≤-zero _ = ≤-zero
Lemma[a≤b≤c→a≤c] (≤-succ r) (≤-succ l) = ≤-succ (Lemma[a≤b≤c→a≤c] r l)

Lemma[a<b≤c→a<c] : ∀{a b c : ℕ} → a < b → b ≤ c → a < c
Lemma[a<b≤c→a<c] = Lemma[a≤b≤c→a≤c]

Lemma[n≤n] : ∀(n : ℕ) → n ≤ n
Lemma[n≤n] 0        = ≤-zero
Lemma[n≤n] (succ n) = ≤-succ (Lemma[n≤n] n)

Lemma[n≤n+1] : ∀(n : ℕ) → n ≤ succ n
Lemma[n≤n+1] 0        = ≤-zero
Lemma[n≤n+1] (succ n) = ≤-succ (Lemma[n≤n+1] n)

Lemma[m+1≤n+1→m≤n] : ∀{m n : ℕ} → succ m ≤ succ n → m ≤ n
Lemma[m+1≤n+1→m≤n] (≤-succ r) = r

Lemma[m≮n→n≤m] : ∀{m n : ℕ} → m ≮ n → n ≤ m
Lemma[m≮n→n≤m] {m}      {0}      f = ≤-zero
Lemma[m≮n→n≤m] {0}      {succ n} f = ∅-elim (f (≤-succ ≤-zero))
Lemma[m≮n→n≤m] {succ m} {succ n} f = ≤-succ (Lemma[m≮n→n≤m] (f ∘ ≤-succ))

Lemma[≤-max] : ∀(n m : ℕ) → (n ≤ maximum n m) ∧ (m ≤ maximum n m)
Lemma[≤-max] 0 0 = ∧-intro ≤-zero ≤-zero
Lemma[≤-max] 0 (succ m) = ∧-intro ≤-zero (≤-succ (∧-elim₁ (Lemma[≤-max] 0 m)))
Lemma[≤-max] (succ n) 0 = ∧-intro (Lemma[n≤n] (succ n)) ≤-zero
Lemma[≤-max] (succ n) (succ m) = ∧-intro (≤-succ (∧-elim₀ (Lemma[≤-max] n m))) (≤-succ (∧-elim₁ (Lemma[≤-max] n m)))

Lemma[m<n→m≠n] : ∀{m n : ℕ} → m < n → m ≠ n
Lemma[m<n→m≠n] {0}      {0}      ()
Lemma[m<n→m≠n] {0}      {succ n} r          = λ ()
Lemma[m<n→m≠n] {succ m} {0}      r          = λ ()
Lemma[m<n→m≠n] {succ m} {succ n} (≤-succ r) = λ e → Lemma[m<n→m≠n] r (succ-injective e)

Lemma[a≤b→a+c≤b+c] : ∀(a b c : ℕ) → a ≤ b → a + c ≤ b + c
Lemma[a≤b→a+c≤b+c] a b 0        r = r
Lemma[a≤b→a+c≤b+c] a b (succ c) r = ≤-succ (Lemma[a≤b→a+c≤b+c] a b c r)

Lemma[a<b→a+c<b+c] : ∀(a b c : ℕ) → a < b → a + c < b + c
Lemma[a<b→a+c<b+c] a b c r = transport {ℕ} {λ n → n ≤ b + c} (lemma a c) (Lemma[a≤b→a+c≤b+c] (succ a) b c r)
 where
  lemma : ∀(n m : ℕ) → (succ n) + m ≡ succ (n + m)
  lemma n 0 = refl
  lemma n (succ m) = ap succ (lemma n m)

Lemma[a≤a+b] : ∀(a b : ℕ) → a ≤ a + b
Lemma[a≤a+b] a 0 = Lemma[n≤n] a
Lemma[a≤a+b] a (succ b) = Lemma[a≤b≤c→a≤c] (Lemma[a≤a+b] a b) (lemma (a + b))
 where
  lemma : ∀(c : ℕ) → c ≤ succ c
  lemma 0 = ≤-zero
  lemma (succ c) = ≤-succ (lemma c)

Lemma[m≤n∧n≤m→m=n] : ∀{m n : ℕ} → m ≤ n → n ≤ m → m ≡ n
Lemma[m≤n∧n≤m→m=n] {0}      {0}      ≤-zero     ≤-zero      = refl
Lemma[m≤n∧n≤m→m=n] {0}      {succ n} ≤-zero     ()
Lemma[m≤n∧n≤m→m=n] {succ m} {0}      ()         ≤-zero
Lemma[m≤n∧n≤m→m=n] {succ m} {succ n} (≤-succ r) (≤-succ r') = ap succ (Lemma[m≤n∧n≤m→m=n] r r')

\end{code}

For any natural numbers m and n, the type n ≤ m is an hprop and a
discrete type.

\begin{code}

Lemma[≤-hprop] : ∀{m n : ℕ} → ∀(r r' : m ≤ n) → r ≡ r'
Lemma[≤-hprop] {0}      {n}      ≤-zero ≤-zero = refl
Lemma[≤-hprop] {succ m} {0}      ()     ()
Lemma[≤-hprop] {succ m} {succ n} (≤-succ r) (≤-succ r') = ap ≤-succ (Lemma[≤-hprop] r r')

≤-discrete : {m n : ℕ} → discrete (m ≤ n)
≤-discrete r r' = in₀ (Lemma[≤-hprop] r r')

\end{code}

The following lemma can be viewed as another definition of ≤.

\begin{code}

Lemma[≤-∃] : ∀(a b : ℕ) → a ≤ b → ∃ \(c : ℕ) → a + c ≡ b
Lemma[≤-∃] 0 b ≤-zero = b , Lemma[0+m=m] b
Lemma[≤-∃] (succ a) 0 ()
Lemma[≤-∃] (succ a) (succ b) (≤-succ r) = c , trans (Lemma[n+1+m=n+m+1] a c) (ap succ eq)
 where
  c : ℕ
  c = π₀ (Lemma[≤-∃] a b r)
  eq : a + c ≡ b
  eq = π₁ (Lemma[≤-∃] a b r)

\end{code}