Strict inequality natural numbers

module elementary-number-theory.strict-inequality-natural-numbers where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions
open import foundation.unit-type
open import foundation.universe-levels

Definition

The strict ordering of the natural numbers

le-ℕ-Prop :     Prop lzero
le-ℕ-Prop m zero-ℕ = empty-Prop
le-ℕ-Prop zero-ℕ (succ-ℕ m) = unit-Prop
le-ℕ-Prop (succ-ℕ n) (succ-ℕ m) = le-ℕ-Prop n m

le-ℕ :     UU lzero
le-ℕ n m = type-Prop (le-ℕ-Prop n m)

is-prop-le-ℕ : (n : )  (m : )  is-prop (le-ℕ n m)
is-prop-le-ℕ n m = is-prop-type-Prop (le-ℕ-Prop n m)

_<_ = le-ℕ

Properties

Concatenating strict inequalities and equalities

concatenate-eq-le-eq-ℕ :
  {x y z w : }  x  y  le-ℕ y z  z  w  le-ℕ x w
concatenate-eq-le-eq-ℕ refl p refl = p

concatenate-eq-le-ℕ :
  {x y z : }  x  y  le-ℕ y z  le-ℕ x z
concatenate-eq-le-ℕ refl p = p

concatenate-le-eq-ℕ :
  {x y z : }  le-ℕ x y  y  z  le-ℕ x z
concatenate-le-eq-ℕ p refl = p

Strict inequality is decidable

is-decidable-le-ℕ :
  (m n : )  is-decidable (le-ℕ m n)
is-decidable-le-ℕ zero-ℕ zero-ℕ = inr id
is-decidable-le-ℕ zero-ℕ (succ-ℕ n) = inl star
is-decidable-le-ℕ (succ-ℕ m) zero-ℕ = inr id
is-decidable-le-ℕ (succ-ℕ m) (succ-ℕ n) = is-decidable-le-ℕ m n

If m < n then n must be nonzero

is-nonzero-le-ℕ : (m n : )  le-ℕ m n  is-nonzero-ℕ n
is-nonzero-le-ℕ m .zero-ℕ () refl

Any nonzero natural number is strictly greater than 0

le-is-nonzero-ℕ : (n : )  is-nonzero-ℕ n  le-ℕ zero-ℕ n
le-is-nonzero-ℕ zero-ℕ H = H refl
le-is-nonzero-ℕ (succ-ℕ n) H = star

No natural number is strictly less than zero

contradiction-le-zero-ℕ :
  (m : )  (le-ℕ m zero-ℕ)  empty
contradiction-le-zero-ℕ zero-ℕ ()
contradiction-le-zero-ℕ (succ-ℕ m) ()

No successor is strictly less than one

contradiction-le-one-ℕ :
  (n : )  le-ℕ (succ-ℕ n) 1  empty
contradiction-le-one-ℕ zero-ℕ ()
contradiction-le-one-ℕ (succ-ℕ n) ()

The strict ordering of the natural numbers is anti-reflexive

anti-reflexive-le-ℕ : (n : )  ¬ (n < n)
anti-reflexive-le-ℕ zero-ℕ ()
anti-reflexive-le-ℕ (succ-ℕ n) = anti-reflexive-le-ℕ n

If x < y then x ≠ y

neq-le-ℕ : {x y : }  le-ℕ x y  ¬ (x  y)
neq-le-ℕ {zero-ℕ} {succ-ℕ y} H = is-nonzero-succ-ℕ y  inv
neq-le-ℕ {succ-ℕ x} {succ-ℕ y} H p = neq-le-ℕ H (is-injective-succ-ℕ p)

Strict inequality is antisymmetric

anti-symmetric-le-ℕ : (m n : )  le-ℕ m n  le-ℕ n m  m  n
anti-symmetric-le-ℕ (succ-ℕ m) (succ-ℕ n) p q =
  ap succ-ℕ (anti-symmetric-le-ℕ m n p q)

The strict ordering of the natural numbers is transitive

transitive-le-ℕ : (n m l : )  (le-ℕ n m)  (le-ℕ m l)  (le-ℕ n l)
transitive-le-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ l) p q = star
transitive-le-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
  transitive-le-ℕ n m l p q

A sharper variant of transitivity

transitive-le-ℕ' :
  (k l m : )  (le-ℕ k l)  (le-ℕ l (succ-ℕ m))  le-ℕ k m
transitive-le-ℕ' zero-ℕ zero-ℕ m () s
transitive-le-ℕ' (succ-ℕ k) zero-ℕ m () s
transitive-le-ℕ' zero-ℕ (succ-ℕ l) zero-ℕ star s =
  ex-falso (contradiction-le-one-ℕ l s)
transitive-le-ℕ' (succ-ℕ k) (succ-ℕ l) zero-ℕ t s =
  ex-falso (contradiction-le-one-ℕ l s)
transitive-le-ℕ' zero-ℕ (succ-ℕ l) (succ-ℕ m) star s = star
transitive-le-ℕ' (succ-ℕ k) (succ-ℕ l) (succ-ℕ m) t s =
  transitive-le-ℕ' k l m t s

Strict inequality is linear

linear-le-ℕ : (x y : )  (le-ℕ x y) + ((x  y) + (le-ℕ y x))
linear-le-ℕ zero-ℕ zero-ℕ = inr (inl refl)
linear-le-ℕ zero-ℕ (succ-ℕ y) = inl star
linear-le-ℕ (succ-ℕ x) zero-ℕ = inr (inr star)
linear-le-ℕ (succ-ℕ x) (succ-ℕ y) =
  map-coprod id (map-coprod (ap succ-ℕ) id) (linear-le-ℕ x y)

n < m if and only if there exists a nonzero natural number l such that n + l = m

subtraction-le-ℕ :
  (n m : )  le-ℕ n m  Σ   l  (is-nonzero-ℕ l) × (l +ℕ n  m))
subtraction-le-ℕ zero-ℕ m p = pair m (pair (is-nonzero-le-ℕ zero-ℕ m p) refl)
subtraction-le-ℕ (succ-ℕ n) (succ-ℕ m) p =
  pair (pr1 P) (pair (pr1 (pr2 P)) (ap succ-ℕ (pr2 (pr2 P))))
  where
  P : Σ   l'  (is-nonzero-ℕ l') × (l' +ℕ n  m))
  P = subtraction-le-ℕ n m p

le-subtraction-ℕ : (n m l : )  is-nonzero-ℕ l  l +ℕ n  m  le-ℕ n m
le-subtraction-ℕ zero-ℕ m l q p =
  tr  x  le-ℕ zero-ℕ x) p (le-is-nonzero-ℕ l q)
le-subtraction-ℕ (succ-ℕ n) (succ-ℕ m) l q p =
  le-subtraction-ℕ n m l q (is-injective-succ-ℕ p)

Any natural number is strictly less than its successor

succ-le-ℕ : (n : )  le-ℕ n (succ-ℕ n)
succ-le-ℕ zero-ℕ = star
succ-le-ℕ (succ-ℕ n) = succ-le-ℕ n

The successor function preserves strict inequality on the right

preserves-le-succ-ℕ :
  (m n : )  le-ℕ m n  le-ℕ m (succ-ℕ n)
preserves-le-succ-ℕ m n H =
  transitive-le-ℕ m n (succ-ℕ n) H (succ-le-ℕ n)

Concatenating strict and nonstrict inequalities

concatenate-leq-le-ℕ :
  {x y z : }  x ≤-ℕ y  le-ℕ y z  le-ℕ x z
concatenate-leq-le-ℕ {zero-ℕ} {zero-ℕ} {succ-ℕ z} H K = star
concatenate-leq-le-ℕ {zero-ℕ} {succ-ℕ y} {succ-ℕ z} H K = star
concatenate-leq-le-ℕ {succ-ℕ x} {succ-ℕ y} {succ-ℕ z} H K =
  concatenate-leq-le-ℕ {x} {y} {z} H K

concatenate-le-leq-ℕ :
  {x y z : }  le-ℕ x y  y ≤-ℕ z  le-ℕ x z
concatenate-le-leq-ℕ {zero-ℕ} {succ-ℕ y} {succ-ℕ z} H K = star
concatenate-le-leq-ℕ {succ-ℕ x} {succ-ℕ y} {succ-ℕ z} H K =
  concatenate-le-leq-ℕ {x} {y} {z} H K

If m < n then n ≰ m

contradiction-le-ℕ : (m n : )  le-ℕ m n  ¬ (n ≤-ℕ m)
contradiction-le-ℕ zero-ℕ (succ-ℕ n) H K = K
contradiction-le-ℕ (succ-ℕ m) (succ-ℕ n) H = contradiction-le-ℕ m n H

If n ≤ m then m ≮ n

contradiction-le-ℕ' : (m n : )  n ≤-ℕ m  ¬ (le-ℕ m n)
contradiction-le-ℕ' m n K H = contradiction-le-ℕ m n H K

If m ≮ n then n ≤ m

leq-not-le-ℕ : (m n : )  ¬ (le-ℕ m n)  n ≤-ℕ m
leq-not-le-ℕ zero-ℕ zero-ℕ H = star
leq-not-le-ℕ zero-ℕ (succ-ℕ n) H = ex-falso (H star)
leq-not-le-ℕ (succ-ℕ m) zero-ℕ H = star
leq-not-le-ℕ (succ-ℕ m) (succ-ℕ n) H = leq-not-le-ℕ m n H

If x < y then x ≤ y

leq-le-ℕ :
  (x y : )  le-ℕ x y  x ≤-ℕ y
leq-le-ℕ zero-ℕ (succ-ℕ y) H = star
leq-le-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-le-ℕ x y H

If x < y + 1 then x ≤ y

leq-le-succ-ℕ :
  (x y : )  le-ℕ x (succ-ℕ y)  x ≤-ℕ y
leq-le-succ-ℕ zero-ℕ y H = star
leq-le-succ-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-le-succ-ℕ x y H

If x < y then x + 1 ≤ y

leq-succ-le-ℕ :
  (x y : )  le-ℕ x y  leq-ℕ (succ-ℕ x) y
leq-succ-le-ℕ zero-ℕ (succ-ℕ y) H = star
leq-succ-le-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-succ-le-ℕ x y H

If x ≤ y then x < y + 1

le-succ-leq-ℕ :
  (x y : )  leq-ℕ x y  le-ℕ x (succ-ℕ y)
le-succ-leq-ℕ zero-ℕ zero-ℕ H = star
le-succ-leq-ℕ zero-ℕ (succ-ℕ y) H = star
le-succ-leq-ℕ (succ-ℕ x) (succ-ℕ y) H = le-succ-leq-ℕ x y H

x ≤ y if and only if (x = y) + (x < y)

eq-or-le-leq-ℕ :
  (x y : )  leq-ℕ x y  ((x  y) + (le-ℕ x y))
eq-or-le-leq-ℕ zero-ℕ zero-ℕ H = inl refl
eq-or-le-leq-ℕ zero-ℕ (succ-ℕ y) H = inr star
eq-or-le-leq-ℕ (succ-ℕ x) (succ-ℕ y) H =
  map-coprod (ap succ-ℕ) id (eq-or-le-leq-ℕ x y H)

eq-or-le-leq-ℕ' :
  (x y : )  leq-ℕ x y  ((y  x) + (le-ℕ x y))
eq-or-le-leq-ℕ' x y H = map-coprod inv id (eq-or-le-leq-ℕ x y H)

leq-eq-or-le-ℕ :
  (x y : )  ((x  y) + (le-ℕ x y))  leq-ℕ x y
leq-eq-or-le-ℕ x .x (inl refl) = refl-leq-ℕ x
leq-eq-or-le-ℕ x y (inr l) = leq-le-ℕ x y l

If x ≤ y and x ≠ y then x < y

le-leq-neq-ℕ : {x y : }  x ≤-ℕ y  ¬ (x  y)  le-ℕ x y
le-leq-neq-ℕ {zero-ℕ} {zero-ℕ} l f = ex-falso (f refl)
le-leq-neq-ℕ {zero-ℕ} {succ-ℕ y} l f = star
le-leq-neq-ℕ {succ-ℕ x} {succ-ℕ y} l f =
  le-leq-neq-ℕ {x} {y} l  p  f (ap succ-ℕ p))