# Inequality of natural numbers

```agda
module elementary-number-theory.inequality-natural-numbers where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.binary-relations
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.function-types
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

open import order-theory.posets
open import order-theory.preorders
```

</details>

## Idea

The relation `≤` on the natural numbers is the unique relation such that `0` is
less than any natural number, and such that `m+1 ≤ n+1` is equivalent to
`m ≤ n`.

## Definitions

### The partial ordering on ℕ

```agda
leq-ℕ :     UU lzero
leq-ℕ zero-ℕ m = unit
leq-ℕ (succ-ℕ n) zero-ℕ = empty
leq-ℕ (succ-ℕ n) (succ-ℕ m) = leq-ℕ n m

infix 30 _≤-ℕ_
_≤-ℕ_ = leq-ℕ
```

### Alternative definition of the partial ordering on ℕ

```agda
data leq-ℕ' :     UU lzero where
  refl-leq-ℕ' : (n : )  leq-ℕ' n n
  propagate-leq-ℕ' : {x y z : }  succ-ℕ y  z  (leq-ℕ' x y)  (leq-ℕ' x z)
```

## Properties

### Inequality on ℕ is a proposition

```agda
is-prop-leq-ℕ :
  (m n : )  is-prop (leq-ℕ m n)
is-prop-leq-ℕ zero-ℕ zero-ℕ = is-prop-unit
is-prop-leq-ℕ zero-ℕ (succ-ℕ n) = is-prop-unit
is-prop-leq-ℕ (succ-ℕ m) zero-ℕ = is-prop-empty
is-prop-leq-ℕ (succ-ℕ m) (succ-ℕ n) = is-prop-leq-ℕ m n

leq-ℕ-Prop :     Prop lzero
pr1 (leq-ℕ-Prop m n) = leq-ℕ m n
pr2 (leq-ℕ-Prop m n) = is-prop-leq-ℕ m n
```

### The partial ordering on the natural numbers is decidable

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

### The partial ordering on ℕ is a congruence

```agda
concatenate-eq-leq-eq-ℕ :
  {x' x y y' : }  x'  x  x ≤-ℕ y  y  y'  x' ≤-ℕ y'
concatenate-eq-leq-eq-ℕ refl H refl = H

concatenate-leq-eq-ℕ :
  (m : ) {n n' : }  m ≤-ℕ n  n  n'  m ≤-ℕ n'
concatenate-leq-eq-ℕ m H refl = H

concatenate-eq-leq-ℕ :
  {m m' : } (n : )  m'  m  m ≤-ℕ n  m' ≤-ℕ n
concatenate-eq-leq-ℕ n refl H = H
```

### Reflexivity

```agda
refl-leq-ℕ : (n : )  n ≤-ℕ n
refl-leq-ℕ zero-ℕ = star
refl-leq-ℕ (succ-ℕ n) = refl-leq-ℕ n

leq-eq-ℕ : (m n : )  m  n  m ≤-ℕ n
leq-eq-ℕ m .m refl = refl-leq-ℕ m
```

### Transitivity

```agda
transitive-leq-ℕ : is-transitive leq-ℕ
transitive-leq-ℕ zero-ℕ m l p q = star
transitive-leq-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
  transitive-leq-ℕ n m l p q
```

### Antisymmetry

```agda
antisymmetric-leq-ℕ : (m n : )  m ≤-ℕ n  n ≤-ℕ m  m  n
antisymmetric-leq-ℕ zero-ℕ zero-ℕ p q = refl
antisymmetric-leq-ℕ (succ-ℕ m) (succ-ℕ n) p q =
  ap succ-ℕ (antisymmetric-leq-ℕ m n p q)
```

### The poset of natural numbers

```agda
ℕ-Preorder : Preorder lzero lzero
pr1 ℕ-Preorder = 
pr1 (pr2 ℕ-Preorder) = leq-ℕ-Prop
pr1 (pr2 (pr2 ℕ-Preorder)) = refl-leq-ℕ
pr2 (pr2 (pr2 ℕ-Preorder)) = transitive-leq-ℕ

ℕ-Poset : Poset lzero lzero
pr1 ℕ-Poset = ℕ-Preorder
pr2 ℕ-Poset = antisymmetric-leq-ℕ
```

### For any two natural numbers we can decide which one is less than the other

```agda
linear-leq-ℕ :
  (m n : )  (m ≤-ℕ n) + (n ≤-ℕ m)
linear-leq-ℕ zero-ℕ zero-ℕ = inl star
linear-leq-ℕ zero-ℕ (succ-ℕ n) = inl star
linear-leq-ℕ (succ-ℕ m) zero-ℕ = inr star
linear-leq-ℕ (succ-ℕ m) (succ-ℕ n) = linear-leq-ℕ m n
```

### For any three natural numbers, there are three cases in how they can be ordered

```agda
cases-order-three-elements-ℕ :
  (x y z : )  UU lzero
cases-order-three-elements-ℕ x y z =
  ( ( leq-ℕ x y × leq-ℕ y z) +
    ( leq-ℕ x z × leq-ℕ z y)) +
  ( ( ( leq-ℕ y z × leq-ℕ z x) +
      ( leq-ℕ y x × leq-ℕ x z)) +
    ( ( leq-ℕ z x × leq-ℕ x y) +
      ( leq-ℕ z y × leq-ℕ y x)))

order-three-elements-ℕ :
  (x y z : )  cases-order-three-elements-ℕ x y z
order-three-elements-ℕ zero-ℕ zero-ℕ zero-ℕ = inl (inl (pair star star))
order-three-elements-ℕ zero-ℕ zero-ℕ (succ-ℕ z) = inl (inl (pair star star))
order-three-elements-ℕ zero-ℕ (succ-ℕ y) zero-ℕ = inl (inr (pair star star))
order-three-elements-ℕ zero-ℕ (succ-ℕ y) (succ-ℕ z) =
  inl (map-coprod (pair star) (pair star) (linear-leq-ℕ y z))
order-three-elements-ℕ (succ-ℕ x) zero-ℕ zero-ℕ =
  inr (inl (inl (pair star star)))
order-three-elements-ℕ (succ-ℕ x) zero-ℕ (succ-ℕ z) =
  inr (inl (map-coprod (pair star) (pair star) (linear-leq-ℕ z x)))
order-three-elements-ℕ (succ-ℕ x) (succ-ℕ y) zero-ℕ =
  inr (inr (map-coprod (pair star) (pair star) (linear-leq-ℕ x y)))
order-three-elements-ℕ (succ-ℕ x) (succ-ℕ y) (succ-ℕ z) =
  order-three-elements-ℕ x y z
```

### Zero is less than or equal to any natural number

```agda
leq-zero-ℕ :
  (n : )  zero-ℕ ≤-ℕ n
leq-zero-ℕ n = star
```

### Any natural number less than zero is zero

```agda
is-zero-leq-zero-ℕ :
  (x : )  x ≤-ℕ zero-ℕ  is-zero-ℕ x
is-zero-leq-zero-ℕ zero-ℕ star = refl

is-zero-leq-zero-ℕ' :
  (x : )  x ≤-ℕ zero-ℕ  is-zero-ℕ' x
is-zero-leq-zero-ℕ' zero-ℕ star = refl
```

### Any number is nonzero natural number if it is at least `1`

```agda
leq-one-is-nonzero-ℕ :
  (x : )  is-nonzero-ℕ x  leq-ℕ 1 x
leq-one-is-nonzero-ℕ zero-ℕ H = ex-falso (H refl)
leq-one-is-nonzero-ℕ (succ-ℕ x) H = star

is-nonzero-leq-one-ℕ :
  (x : )  leq-ℕ 1 x  is-nonzero-ℕ x
is-nonzero-leq-one-ℕ .zero-ℕ () refl
```

### Any natural number is less than or equal to its own successor

```agda
succ-leq-ℕ : (n : )  n ≤-ℕ (succ-ℕ n)
succ-leq-ℕ zero-ℕ = star
succ-leq-ℕ (succ-ℕ n) = succ-leq-ℕ n
```

### An natural number less than `n+1` is either less than `n` or it is `n+1`

```agda
decide-leq-succ-ℕ :
  (m n : )  m ≤-ℕ (succ-ℕ n)  (m ≤-ℕ n) + (m  succ-ℕ n)
decide-leq-succ-ℕ zero-ℕ zero-ℕ l = inl star
decide-leq-succ-ℕ zero-ℕ (succ-ℕ n) l = inl star
decide-leq-succ-ℕ (succ-ℕ m) zero-ℕ l =
  inr (ap succ-ℕ (is-zero-leq-zero-ℕ m l))
decide-leq-succ-ℕ (succ-ℕ m) (succ-ℕ n) l =
  map-coprod id (ap succ-ℕ) (decide-leq-succ-ℕ m n l)
```

### If `m` is less than `n`, then it is less than `n+1`

```agda
preserves-leq-succ-ℕ :
  (m n : )  m ≤-ℕ n  m ≤-ℕ (succ-ℕ n)
preserves-leq-succ-ℕ m n p = transitive-leq-ℕ m n (succ-ℕ n) (succ-leq-ℕ n) p
```

### The successor of `n` is not less than or equal to `n`

```agda
neg-succ-leq-ℕ :
  (n : )  ¬ (leq-ℕ (succ-ℕ n) n)
neg-succ-leq-ℕ zero-ℕ = id
neg-succ-leq-ℕ (succ-ℕ n) = neg-succ-leq-ℕ n
```

### If `m ≤ n + 1` then either `m ≤ n` or `m = n + 1`

```agda
cases-leq-succ-ℕ :
  {m n : }  leq-ℕ m (succ-ℕ n)  (leq-ℕ m n) + (m  succ-ℕ n)
cases-leq-succ-ℕ {zero-ℕ} {n} star = inl star
cases-leq-succ-ℕ {succ-ℕ m} {zero-ℕ} p =
  inr (ap succ-ℕ (antisymmetric-leq-ℕ m zero-ℕ p star))
cases-leq-succ-ℕ {succ-ℕ m} {succ-ℕ n} p =
  map-coprod id (ap succ-ℕ) (cases-leq-succ-ℕ p)

cases-leq-succ-reflexive-leq-ℕ :
  {n : }  cases-leq-succ-ℕ {succ-ℕ n} {n} (refl-leq-ℕ n)  inr refl
cases-leq-succ-reflexive-leq-ℕ {zero-ℕ} = refl
cases-leq-succ-reflexive-leq-ℕ {succ-ℕ n} =
  ap (map-coprod id (ap succ-ℕ)) cases-leq-succ-reflexive-leq-ℕ
```

### `m ≤ n` if and only if `n + 1 ≰ m`

```agda
contradiction-leq-ℕ : (m n : )  m ≤-ℕ n  ¬ ((succ-ℕ n) ≤-ℕ m)
contradiction-leq-ℕ (succ-ℕ m) (succ-ℕ n) H K = contradiction-leq-ℕ m n H K

contradiction-leq-ℕ' : (m n : )  (succ-ℕ n) ≤-ℕ m  ¬ (m ≤-ℕ n)
contradiction-leq-ℕ' m n K H = contradiction-leq-ℕ m n H K
```

### Addition preserves inequality

```agda
left-law-leq-add-ℕ :
  (k m n : )  m ≤-ℕ n  (m +ℕ k) ≤-ℕ (n +ℕ k)
left-law-leq-add-ℕ zero-ℕ m n = id
left-law-leq-add-ℕ (succ-ℕ k) m n H = left-law-leq-add-ℕ k m n H

right-law-leq-add-ℕ : (k m n : )  m ≤-ℕ n  (k +ℕ m) ≤-ℕ (k +ℕ n)
right-law-leq-add-ℕ k m n H =
  concatenate-eq-leq-eq-ℕ
    ( commutative-add-ℕ k m)
    ( left-law-leq-add-ℕ k m n H)
    ( commutative-add-ℕ n k)

preserves-leq-add-ℕ :
  {m m' n n' : }  m ≤-ℕ m'  n ≤-ℕ n'  (m +ℕ n) ≤-ℕ (m' +ℕ n')
preserves-leq-add-ℕ {m} {m'} {n} {n'} H K =
  transitive-leq-ℕ
    ( m +ℕ n)
    ( m' +ℕ n)
    ( m' +ℕ n')
    ( right-law-leq-add-ℕ m' n n' K)
    ( left-law-leq-add-ℕ n m m' H)
```

### Addition reflects the ordering on ℕ

```agda
reflects-order-add-ℕ :
  (k m n : )  (m +ℕ k) ≤-ℕ (n +ℕ k)  m ≤-ℕ n
reflects-order-add-ℕ zero-ℕ m n = id
reflects-order-add-ℕ (succ-ℕ k) m n = reflects-order-add-ℕ k m n

reflects-order-add-ℕ' :
  (k m n : )  (k +ℕ m) ≤-ℕ (k +ℕ n)  m ≤-ℕ n
reflects-order-add-ℕ' k m n H =
  reflects-order-add-ℕ k m n
    ( concatenate-eq-leq-eq-ℕ
      ( commutative-add-ℕ m k)
      ( H)
      ( commutative-add-ℕ k n))
```

### `m ≤ m + n` for any two natural numbers `m` and `n`

```agda
leq-add-ℕ : (m n : )  m ≤-ℕ (m +ℕ n)
leq-add-ℕ m zero-ℕ = refl-leq-ℕ m
leq-add-ℕ m (succ-ℕ n) =
  transitive-leq-ℕ
    ( m)
    ( m +ℕ n)
    ( succ-ℕ (m +ℕ n))
    ( succ-leq-ℕ (m +ℕ n))
    ( leq-add-ℕ m n)

leq-add-ℕ' : (m n : )  m ≤-ℕ (n +ℕ m)
leq-add-ℕ' m n =
  concatenate-leq-eq-ℕ m (leq-add-ℕ m n) (commutative-add-ℕ m n)
```

### We have `n ≤ m` if and only if there is a number `l` such that `l+n=m`

```agda
subtraction-leq-ℕ : (n m : )  n ≤-ℕ m  Σ   l  l +ℕ n  m)
subtraction-leq-ℕ zero-ℕ m p = pair m refl
subtraction-leq-ℕ (succ-ℕ n) (succ-ℕ m) p = pair (pr1 P) (ap succ-ℕ (pr2 P))
  where
  P : Σ   l'  l' +ℕ n  m)
  P = subtraction-leq-ℕ n m p

leq-subtraction-ℕ : (n m l : )  l +ℕ n  m  n ≤-ℕ m
leq-subtraction-ℕ zero-ℕ m l p = leq-zero-ℕ m
leq-subtraction-ℕ (succ-ℕ n) (succ-ℕ m) l p =
  leq-subtraction-ℕ n m l (is-injective-succ-ℕ p)
```

### Multiplication preserves the ordering on ℕ

```agda
preserves-order-mul-ℕ :
  (k m n : )  m ≤-ℕ n  (m *ℕ k) ≤-ℕ (n *ℕ k)
preserves-order-mul-ℕ k zero-ℕ n p = star
preserves-order-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p =
  left-law-leq-add-ℕ k
    ( m *ℕ k)
    ( n *ℕ k)
    ( preserves-order-mul-ℕ k m n p)

preserves-order-mul-ℕ' :
  (k m n : )  m ≤-ℕ n  (k *ℕ m) ≤-ℕ (k *ℕ n)
preserves-order-mul-ℕ' k m n H =
  concatenate-eq-leq-eq-ℕ
    ( commutative-mul-ℕ k m)
    ( preserves-order-mul-ℕ k m n H)
    ( commutative-mul-ℕ n k)
```

### Multiplication preserves inequality

```agda
preserves-leq-mul-ℕ :
  (m m' n n' : )  m ≤-ℕ m'  n ≤-ℕ n'  (m *ℕ n) ≤-ℕ (m' *ℕ n')
preserves-leq-mul-ℕ m m' n n' H K =
  transitive-leq-ℕ
    ( m *ℕ n)
    ( m' *ℕ n)
    ( m' *ℕ n')
    ( preserves-order-mul-ℕ' m' n n' K)
    ( preserves-order-mul-ℕ n m m' H)
```

### Multiplication by a nonzero element reflects the ordering on ℕ

```agda
reflects-order-mul-ℕ :
  (k m n : )  (m *ℕ (succ-ℕ k)) ≤-ℕ (n *ℕ (succ-ℕ k))  m ≤-ℕ n
reflects-order-mul-ℕ k zero-ℕ n p = star
reflects-order-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p =
  reflects-order-mul-ℕ k m n
    ( reflects-order-add-ℕ
      ( succ-ℕ k)
      ( m *ℕ (succ-ℕ k))
      ( n *ℕ (succ-ℕ k))
      ( p))

reflects-order-mul-ℕ' :
  (k m n : )  ((succ-ℕ k) *ℕ m) ≤-ℕ ((succ-ℕ k) *ℕ n)  m ≤-ℕ n
reflects-order-mul-ℕ' k m n H =
  reflects-order-mul-ℕ k m n
    ( concatenate-eq-leq-eq-ℕ
      ( commutative-mul-ℕ m (succ-ℕ k))
      ( H)
      ( commutative-mul-ℕ (succ-ℕ k) n))
```

### Any number `x` is less than a nonzero multiple of itself

```agda
leq-mul-ℕ :
  (k x : )  x ≤-ℕ (x *ℕ (succ-ℕ k))
leq-mul-ℕ k x =
  concatenate-eq-leq-ℕ
    ( x *ℕ (succ-ℕ k))
    ( inv (right-unit-law-mul-ℕ x))
    ( preserves-order-mul-ℕ' x 1 (succ-ℕ k) (leq-zero-ℕ k))

leq-mul-ℕ' :
  (k x : )  x ≤-ℕ ((succ-ℕ k) *ℕ x)
leq-mul-ℕ' k x =
  concatenate-leq-eq-ℕ x
    ( leq-mul-ℕ k x)
    ( commutative-mul-ℕ x (succ-ℕ k))

leq-mul-is-nonzero-ℕ :
  (k x : )  is-nonzero-ℕ k  x ≤-ℕ (x *ℕ k)
leq-mul-is-nonzero-ℕ k x H with is-successor-is-nonzero-ℕ H
... | pair l refl = leq-mul-ℕ l x

leq-mul-is-nonzero-ℕ' :
  (k x : )  is-nonzero-ℕ k  x ≤-ℕ (k *ℕ x)
leq-mul-is-nonzero-ℕ' k x H with is-successor-is-nonzero-ℕ H
... | pair l refl = leq-mul-ℕ' l x
```

## See also

- Strict inequality of the natural numbers is defined in
  [`strict-inequality-natural-numbers`](elementary-number-theory.strict-inequality-natural-numbers.md)