# 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  _≤-ℕ_
_≤-ℕ_ = 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-ℕ  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-ℕ  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  (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)