# Inequality of natural numbers

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Eléonore Mangel, Bryan Lu, Julian KG, Victor Blanchi, fernabnor, louismntnu and malarbol.

Created on 2022-01-26.

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

Imports
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


## 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

### Inequality on the natural numbers

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 inequality on the natural numbers

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 the natural numbers is a proposition

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


### Inequality on the natural numbers is decidable

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


### Inequality on the natural numbers is a congruence

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


### Inequality on the natural numbers is reflexive

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


### Inequality on the natural numbers is transitive

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


### Inequality on the natural numbers is antisymmetric

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 partially ordered set of natural numbers ordered by inequality

ℕ-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

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

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-coproduct (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-coproduct (pair star) (pair star) (linear-leq-ℕ z x)))
order-three-elements-ℕ (succ-ℕ x) (succ-ℕ y) zero-ℕ =
inr (inr (map-coproduct (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

leq-zero-ℕ :
(n : ℕ) → zero-ℕ ≤-ℕ n
leq-zero-ℕ n = star


### Any natural number less than zero is zero

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

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

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


### Any natural number less than or equal to n+1 is either less than or equal to n or it is n+1

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-coproduct id (ap succ-ℕ) (decide-leq-succ-ℕ m n l)


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

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

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

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-coproduct 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-coproduct id (ap succ-ℕ)) cases-leq-succ-reflexive-leq-ℕ


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

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)


### Addition preserves inequality of natural numbers

preserves-leq-left-add-ℕ :
(k m n : ℕ) → m ≤-ℕ n → (m +ℕ k) ≤-ℕ (n +ℕ k)
preserves-leq-left-add-ℕ zero-ℕ m n = id
preserves-leq-left-add-ℕ (succ-ℕ k) m n H = preserves-leq-left-add-ℕ k m n H

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

{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')
( preserves-leq-right-add-ℕ m' n n' K)
( preserves-leq-left-add-ℕ n m m' H)


### Addition reflects inequality of natural numbers

reflects-leq-left-add-ℕ :
(k m n : ℕ) → (m +ℕ k) ≤-ℕ (n +ℕ k) → m ≤-ℕ n
reflects-leq-left-add-ℕ zero-ℕ m n = id

(k m n : ℕ) → (k +ℕ m) ≤-ℕ (k +ℕ n) → m ≤-ℕ n
reflects-leq-right-add-ℕ k m n H =
( concatenate-eq-leq-eq-ℕ
( H)


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

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

leq-add-ℕ' : (m n : ℕ) → m ≤-ℕ (n +ℕ m)


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

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 inequality of natural numbers

preserves-leq-left-mul-ℕ :
(k m n : ℕ) → m ≤-ℕ n → (m *ℕ k) ≤-ℕ (n *ℕ k)
preserves-leq-left-mul-ℕ k zero-ℕ n p = star
preserves-leq-left-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p =
( m *ℕ k)
( n *ℕ k)
( preserves-leq-left-mul-ℕ k m n p)

preserves-leq-right-mul-ℕ :
(k m n : ℕ) → m ≤-ℕ n → (k *ℕ m) ≤-ℕ (k *ℕ n)
preserves-leq-right-mul-ℕ k m n H =
concatenate-eq-leq-eq-ℕ
( commutative-mul-ℕ k m)
( preserves-leq-left-mul-ℕ k m n H)
( commutative-mul-ℕ n k)

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-leq-right-mul-ℕ m' n n' K)
( preserves-leq-left-mul-ℕ n m m' H)


### Multiplication by a nonzero natural number reflects inequality of natural numbers

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
( 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

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-leq-right-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