# Divisibility of natural numbers

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

<details><summary>Imports</summary>

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

open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.negated-equality
open import foundation.negation
open import foundation.propositional-maps
open import foundation.propositions
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-empty-type
open import foundation.unit-type
open import foundation.universe-levels
```

</details>

## Idea

A natural number `m` is said to **divide** a natural number `n` if there exists
a natural number `k` equipped with an identification `km = n`. Using the
Curry-Howard interpretation of logic into type theory, we express divisibility
as follows:

```text
  div-ℕ m n := Σ (k : ℕ), k *ℕ m = n.
```

If `n` is a nonzero natural number, then `div-ℕ m n` is always a proposition in
the sense that the type `div-ℕ m n` contains at most one element.

## Definitions

```agda
div-ℕ :     UU lzero
div-ℕ m n = Σ   k  k *ℕ m  n)

quotient-div-ℕ : (x y : )  div-ℕ x y  
quotient-div-ℕ x y H = pr1 H

eq-quotient-div-ℕ :
  (x y : ) (H : div-ℕ x y)  (quotient-div-ℕ x y H) *ℕ x  y
eq-quotient-div-ℕ x y H = pr2 H

eq-quotient-div-ℕ' :
  (x y : ) (H : div-ℕ x y)  x *ℕ (quotient-div-ℕ x y H)  y
eq-quotient-div-ℕ' x y H =
  commutative-mul-ℕ x (quotient-div-ℕ x y H)  eq-quotient-div-ℕ x y H

div-quotient-div-ℕ :
  (d x : ) (H : div-ℕ d x)  div-ℕ (quotient-div-ℕ d x H) x
pr1 (div-quotient-div-ℕ d x (u , p)) = d
pr2 (div-quotient-div-ℕ d x (u , p)) = commutative-mul-ℕ d u  p
```

### Concatenating equality and divisibility

```agda
concatenate-eq-div-ℕ :
  {x y z : }  x  y  div-ℕ y z  div-ℕ x z
concatenate-eq-div-ℕ refl p = p

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

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

## Properties

### The quotients of a natural number `n` by two natural numbers `p` and `q` are equal if `p` and `q` are equal

```agda
eq-quotient-div-eq-div-ℕ :
  (x y z : )  is-nonzero-ℕ x  x  y 
  (H : div-ℕ x z)  (I : div-ℕ y z) 
  quotient-div-ℕ x z H  quotient-div-ℕ y z I
eq-quotient-div-eq-div-ℕ x y z n e H I =
  is-injective-left-mul-ℕ
    ( x)
    ( n)
  ( tr
    ( λ p 
      x *ℕ (quotient-div-ℕ x z H) 
      p *ℕ (quotient-div-ℕ y z I))
    ( inv e)
    ( commutative-mul-ℕ x (quotient-div-ℕ x z H) 
      ( eq-quotient-div-ℕ x z H 
        ( inv (eq-quotient-div-ℕ y z I) 
          commutative-mul-ℕ (quotient-div-ℕ y z I) y))))
```

### Divisibility by a nonzero natural number is a property

```agda
is-prop-div-ℕ : (k x : )  is-nonzero-ℕ k  is-prop (div-ℕ k x)
is-prop-div-ℕ k x f = is-prop-map-is-emb (is-emb-right-mul-ℕ k f) x
```

### The divisibility relation is a partial order on the natural numbers

```agda
refl-div-ℕ : is-reflexive div-ℕ
pr1 (refl-div-ℕ x) = 1
pr2 (refl-div-ℕ x) = left-unit-law-mul-ℕ x

div-eq-ℕ : (x y : )  x  y  div-ℕ x y
div-eq-ℕ x .x refl = refl-div-ℕ x

antisymmetric-div-ℕ : is-antisymmetric div-ℕ
antisymmetric-div-ℕ zero-ℕ zero-ℕ H K = refl
antisymmetric-div-ℕ zero-ℕ (succ-ℕ y) (pair k p) K =
  inv (right-zero-law-mul-ℕ k)  p
antisymmetric-div-ℕ (succ-ℕ x) zero-ℕ H (pair l q) =
  inv q  right-zero-law-mul-ℕ l
antisymmetric-div-ℕ (succ-ℕ x) (succ-ℕ y) (pair k p) (pair l q) =
  ( inv (left-unit-law-mul-ℕ (succ-ℕ x))) 
  ( ( ap
      ( _*ℕ (succ-ℕ x))
      ( inv
        ( is-one-right-is-one-mul-ℕ l k
          ( is-one-is-left-unit-mul-ℕ (l *ℕ k) x
            ( ( associative-mul-ℕ l k (succ-ℕ x)) 
              ( ap (l *ℕ_) p  q)))))) 
    ( p))

transitive-div-ℕ : is-transitive div-ℕ
pr1 (transitive-div-ℕ x y z (pair l q) (pair k p)) = l *ℕ k
pr2 (transitive-div-ℕ x y z (pair l q) (pair k p)) =
  associative-mul-ℕ l k x  (ap (l *ℕ_) p  q)
```

### If `x` is nonzero and `d | x`, then `d ≤ x`

```agda
leq-div-succ-ℕ : (d x : )  div-ℕ d (succ-ℕ x)  leq-ℕ d (succ-ℕ x)
leq-div-succ-ℕ d x (pair (succ-ℕ k) p) =
  concatenate-leq-eq-ℕ d (leq-mul-ℕ' k d) p

leq-div-ℕ : (d x : )  is-nonzero-ℕ x  div-ℕ d x  leq-ℕ d x
leq-div-ℕ d x f H with is-successor-is-nonzero-ℕ f
... | (pair y refl) = leq-div-succ-ℕ d y H

leq-quotient-div-ℕ :
  (d x : )  is-nonzero-ℕ x  (H : div-ℕ d x)  leq-ℕ (quotient-div-ℕ d x H) x
leq-quotient-div-ℕ d x f H =
  leq-div-ℕ (quotient-div-ℕ d x H) x f (div-quotient-div-ℕ d x H)

leq-quotient-div-ℕ' :
  (d x : )  is-nonzero-ℕ d  (H : div-ℕ d x)  leq-ℕ (quotient-div-ℕ d x H) x
leq-quotient-div-ℕ' d zero-ℕ f (zero-ℕ , p) = star
leq-quotient-div-ℕ' d zero-ℕ f (succ-ℕ n , p) =
  f (is-zero-right-is-zero-add-ℕ _ d p)
leq-quotient-div-ℕ' d (succ-ℕ x) f H =
  leq-quotient-div-ℕ d (succ-ℕ x) (is-nonzero-succ-ℕ x) H
```

### If `x` is nonzero, if `d | x` and `d ≠ x`, then `d < x`

```agda
le-div-succ-ℕ :
  (d x : )  div-ℕ d (succ-ℕ x)  d  succ-ℕ x  le-ℕ d (succ-ℕ x)
le-div-succ-ℕ d x H f = le-leq-neq-ℕ (leq-div-succ-ℕ d x H) f

le-div-ℕ : (d x : )  is-nonzero-ℕ x  div-ℕ d x  d  x  le-ℕ d x
le-div-ℕ d x H K f = le-leq-neq-ℕ (leq-div-ℕ d x H K) f
```

### `1` divides any number

```agda
div-one-ℕ :
  (x : )  div-ℕ 1 x
pr1 (div-one-ℕ x) = x
pr2 (div-one-ℕ x) = right-unit-law-mul-ℕ x

div-is-one-ℕ :
  (k x : )  is-one-ℕ k  div-ℕ k x
div-is-one-ℕ .1 x refl = div-one-ℕ x
```

### `x | 1` implies `x = 1`

```agda
is-one-div-one-ℕ : (x : )  div-ℕ x 1  is-one-ℕ x
is-one-div-one-ℕ x H = antisymmetric-div-ℕ x 1 H (div-one-ℕ x)
```

### Any number divides `0`

```agda
div-zero-ℕ :
  (k : )  div-ℕ k 0
pr1 (div-zero-ℕ k) = 0
pr2 (div-zero-ℕ k) = left-zero-law-mul-ℕ k

div-is-zero-ℕ :
  (k x : )  is-zero-ℕ x  div-ℕ k x
div-is-zero-ℕ k .zero-ℕ refl = div-zero-ℕ k
```

### `0 | x` implies `x = 0` and `x | 1` implies `x = 1`

```agda
is-zero-div-zero-ℕ : (x : )  div-ℕ zero-ℕ x  is-zero-ℕ x
is-zero-div-zero-ℕ x H = antisymmetric-div-ℕ x zero-ℕ (div-zero-ℕ x) H

is-zero-is-zero-div-ℕ : (x y : )  div-ℕ x y  is-zero-ℕ x  is-zero-ℕ y
is-zero-is-zero-div-ℕ .zero-ℕ y d refl = is-zero-div-zero-ℕ y d
```

### Any divisor of a nonzero number is nonzero

```agda
is-nonzero-div-ℕ :
  (d x : )  div-ℕ d x  is-nonzero-ℕ x  is-nonzero-ℕ d
is-nonzero-div-ℕ .zero-ℕ x H K refl = K (is-zero-div-zero-ℕ x H)
```

### Any divisor of a number at least `1` is at least `1`

```agda
leq-one-div-ℕ :
  (d x : )  div-ℕ d x  leq-ℕ 1 x  leq-ℕ 1 d
leq-one-div-ℕ d x H L =
  leq-one-is-nonzero-ℕ d (is-nonzero-div-ℕ d x H (is-nonzero-leq-one-ℕ x L))
```

### If `x < d` and `d | x`, then `x` must be `0`

```agda
is-zero-div-ℕ :
  (d x : )  le-ℕ x d  div-ℕ d x  is-zero-ℕ x
is-zero-div-ℕ d zero-ℕ H D = refl
is-zero-div-ℕ d (succ-ℕ x) H (pair (succ-ℕ k) p) =
  ex-falso
    ( contradiction-le-ℕ
      ( succ-ℕ x) d H
      ( concatenate-leq-eq-ℕ d
        ( leq-add-ℕ' d (k *ℕ d)) p))
```

### If `x` divides `y` then `x` divides any multiple of `y`

```agda
div-mul-ℕ :
  (k x y : )  div-ℕ x y  div-ℕ x (k *ℕ y)
div-mul-ℕ k x y H =
  transitive-div-ℕ x y (k *ℕ y) (pair k refl) H

div-mul-ℕ' :
  (k x y : )  div-ℕ x y  div-ℕ x (y *ℕ k)
div-mul-ℕ' k x y H =
  tr (div-ℕ x) (commutative-mul-ℕ k y) (div-mul-ℕ k x y H)
```

### A 3-for-2 property of division with respect to addition

```agda
div-add-ℕ :
  (d x y : )  div-ℕ d x  div-ℕ d y  div-ℕ d (x +ℕ y)
pr1 (div-add-ℕ d x y (pair n p) (pair m q)) = n +ℕ m
pr2 (div-add-ℕ d x y (pair n p) (pair m q)) =
  ( right-distributive-mul-add-ℕ n m d) 
  ( ap-add-ℕ p q)

div-left-summand-ℕ :
  (d x y : )  div-ℕ d y  div-ℕ d (x +ℕ y)  div-ℕ d x
div-left-summand-ℕ zero-ℕ x y (pair m q) (pair n p) =
  pair zero-ℕ
    ( ( inv (right-zero-law-mul-ℕ n)) 
      ( p  (ap (x +ℕ_) ((inv q)  (right-zero-law-mul-ℕ m)))))
pr1 (div-left-summand-ℕ (succ-ℕ d) x y (pair m q) (pair n p)) = dist-ℕ m n
pr2 (div-left-summand-ℕ (succ-ℕ d) x y (pair m q) (pair n p)) =
  is-injective-right-add-ℕ (m *ℕ (succ-ℕ d))
    ( ( inv
        ( ( right-distributive-mul-add-ℕ m (dist-ℕ m n) (succ-ℕ d)) 
          ( commutative-add-ℕ
            ( m *ℕ (succ-ℕ d))
            ( (dist-ℕ m n) *ℕ (succ-ℕ d))))) 
      ( ( ap
          ( _*ℕ (succ-ℕ d))
          ( is-additive-right-inverse-dist-ℕ m n
            ( reflects-order-mul-ℕ d m n
              ( concatenate-eq-leq-eq-ℕ q
                ( leq-add-ℕ' y x)
                ( inv p))))) 
        ( p  (ap (x +ℕ_) (inv q)))))

div-right-summand-ℕ :
  (d x y : )  div-ℕ d x  div-ℕ d (x +ℕ y)  div-ℕ d y
div-right-summand-ℕ d x y H1 H2 =
  div-left-summand-ℕ d y x H1 (concatenate-div-eq-ℕ H2 (commutative-add-ℕ x y))
```

### If `d` divides both `x` and `x + 1`, then `d = 1`

```agda
is-one-div-ℕ : (x y : )  div-ℕ x y  div-ℕ x (succ-ℕ y)  is-one-ℕ x
is-one-div-ℕ x y H K = is-one-div-one-ℕ x (div-right-summand-ℕ x y 1 H K)
```

### Multiplication preserves divisibility

```agda
preserves-div-mul-ℕ :
  (k x y : )  div-ℕ x y  div-ℕ (k *ℕ x) (k *ℕ y)
pr1 (preserves-div-mul-ℕ k x y (pair q p)) = q
pr2 (preserves-div-mul-ℕ k x y (pair q p)) =
  ( inv (associative-mul-ℕ q k x)) 
    ( ( ap (_*ℕ x) (commutative-mul-ℕ q k)) 
      ( ( associative-mul-ℕ k q x) 
        ( ap (k *ℕ_) p)))
```

### Multiplication by a nonzero number reflects divisibility

```agda
reflects-div-mul-ℕ :
  (k x y : )  is-nonzero-ℕ k  div-ℕ (k *ℕ x) (k *ℕ y)  div-ℕ x y
pr1 (reflects-div-mul-ℕ k x y H (pair q p)) = q
pr2 (reflects-div-mul-ℕ k x y H (pair q p)) =
  is-injective-left-mul-ℕ k H
    ( ( inv (associative-mul-ℕ k q x)) 
      ( ( ap (_*ℕ x) (commutative-mul-ℕ k q)) 
        ( ( associative-mul-ℕ q k x) 
          ( p))))
```

### If a nonzero number `d` divides `y`, then `dx` divides `y` if and only if `x` divides the quotient `y/d`

```agda
div-quotient-div-div-ℕ :
  (x y d : ) (H : div-ℕ d y)  is-nonzero-ℕ d 
  div-ℕ (d *ℕ x) y  div-ℕ x (quotient-div-ℕ d y H)
div-quotient-div-div-ℕ x y d H f K =
  reflects-div-mul-ℕ d x
    ( quotient-div-ℕ d y H)
    ( f)
    ( tr (div-ℕ (d *ℕ x)) (inv (eq-quotient-div-ℕ' d y H)) K)

div-div-quotient-div-ℕ :
  (x y d : ) (H : div-ℕ d y) 
  div-ℕ x (quotient-div-ℕ d y H)  div-ℕ (d *ℕ x) y
div-div-quotient-div-ℕ x y d H K =
  tr
    ( div-ℕ (d *ℕ x))
    ( eq-quotient-div-ℕ' d y H)
    ( preserves-div-mul-ℕ d x (quotient-div-ℕ d y H) K)
```

### If `d` divides a nonzero number `x`, then the quotient `x/d` is also nonzero

```agda
is-nonzero-quotient-div-ℕ :
  {d x : } (H : div-ℕ d x) 
  is-nonzero-ℕ x  is-nonzero-ℕ (quotient-div-ℕ d x H)
is-nonzero-quotient-div-ℕ {d} {.(k *ℕ d)} (pair k refl) =
  is-nonzero-left-factor-mul-ℕ k d
```

### If `d` divides a number `1 ≤ x`, then `1 ≤ x/d`

```agda
leq-one-quotient-div-ℕ :
  (d x : ) (H : div-ℕ d x)  leq-ℕ 1 x  leq-ℕ 1 (quotient-div-ℕ d x H)
leq-one-quotient-div-ℕ d x H K =
  leq-one-div-ℕ
    ( quotient-div-ℕ d x H)
    ( x)
    ( div-quotient-div-ℕ d x H)
    ( K)
```

### `a/a = 1`

```agda
is-idempotent-quotient-div-ℕ :
  (a : )  is-nonzero-ℕ a  (H : div-ℕ a a)  is-one-ℕ (quotient-div-ℕ a a H)
is-idempotent-quotient-div-ℕ zero-ℕ nz (u , p) = ex-falso (nz refl)
is-idempotent-quotient-div-ℕ (succ-ℕ a) nz (u , p) =
  is-one-is-left-unit-mul-ℕ u a p
```

### If `b` divides `a` and `c` divides `b` and `c` is nonzero, then `a/b · b/c = a/c`

```agda
simplify-mul-quotient-div-ℕ :
  {a b c : }  is-nonzero-ℕ c 
  (H : div-ℕ b a) (K : div-ℕ c b) (L : div-ℕ c a) 
  ( (quotient-div-ℕ b a H) *ℕ (quotient-div-ℕ c b K)) 
  ( quotient-div-ℕ c a L)
simplify-mul-quotient-div-ℕ {a} {b} {c} nz H K L =
  is-injective-right-mul-ℕ c nz
    ( equational-reasoning
      (a/b *ℕ b/c) *ℕ c
       a/b *ℕ (b/c *ℕ c)
        by associative-mul-ℕ a/b b/c c
       a/b *ℕ b
        by ap (a/b *ℕ_) (eq-quotient-div-ℕ c b K)
       a
        by eq-quotient-div-ℕ b a H
       a/c *ℕ c
        by inv (eq-quotient-div-ℕ c a L))
  where
  a/b : 
  a/b = quotient-div-ℕ b a H
  b/c : 
  b/c = quotient-div-ℕ c b K
  a/c : 
  a/c = quotient-div-ℕ c a L
```

### If `d | a` and `d` is nonzero, then `x | a/d` if and only if `xd | a`

```agda
simplify-div-quotient-div-ℕ :
  {a d x : }  is-nonzero-ℕ d  (H : div-ℕ d a) 
  (div-ℕ x (quotient-div-ℕ d a H))  (div-ℕ (x *ℕ d) a)
pr1 (pr1 (simplify-div-quotient-div-ℕ nz H) (u , p)) = u
pr2 (pr1 (simplify-div-quotient-div-ℕ {a} {d} {x} nz H) (u , p)) =
  equational-reasoning
    u *ℕ (x *ℕ d)
     (u *ℕ x) *ℕ d
      by inv (associative-mul-ℕ u x d)
     (quotient-div-ℕ d a H) *ℕ d
      by ap (_*ℕ d) p
     a
      by eq-quotient-div-ℕ d a H
pr1 (pr2 (simplify-div-quotient-div-ℕ nz H) (u , p)) = u
pr2 (pr2 (simplify-div-quotient-div-ℕ {a} {d} {x} nz H) (u , p)) =
  is-injective-right-mul-ℕ d nz
    ( equational-reasoning
        (u *ℕ x) *ℕ d
         u *ℕ (x *ℕ d)
          by associative-mul-ℕ u x d
         a
          by p
         (quotient-div-ℕ d a H) *ℕ d
          by inv (eq-quotient-div-ℕ d a H))
```

### Suppose `H : b | a` and `K : c | b`, where `c` is nonzero. If `d` divides `b/c` then `d` divides `a/c`

```agda
div-quotient-div-div-quotient-div-ℕ :
  {a b c d : }  is-nonzero-ℕ c  (H : div-ℕ b a)
  (K : div-ℕ c b) (L : div-ℕ c a) 
  div-ℕ d (quotient-div-ℕ c b K) 
  div-ℕ d (quotient-div-ℕ c a L)
div-quotient-div-div-quotient-div-ℕ {a} {b} {c} {d} nz H K L M =
  tr
    ( div-ℕ d)
    ( simplify-mul-quotient-div-ℕ nz H K L)
    ( div-mul-ℕ
      ( quotient-div-ℕ b a H)
      ( d)
      ( quotient-div-ℕ c b K)
      ( M))
```

### If `x` is nonzero and `d | x`, then `x/d = 1` if and only if `d = x`

```agda
is-one-quotient-div-ℕ :
  (d x : )  is-nonzero-ℕ x  (H : div-ℕ d x)  (d  x) 
  is-one-ℕ (quotient-div-ℕ d x H)
is-one-quotient-div-ℕ d .d f H refl = is-idempotent-quotient-div-ℕ d f H

eq-is-one-quotient-div-ℕ :
  (d x : )  (H : div-ℕ d x)  is-one-ℕ (quotient-div-ℕ d x H)  d  x
eq-is-one-quotient-div-ℕ d x (.1 , q) refl = inv (left-unit-law-mul-ℕ d)  q
```

### If `x` is nonzero and `d | x`, then `x/d = x` if and only if `d = 1`

```agda
compute-quotient-div-is-one-ℕ :
  (d x : )  (H : div-ℕ d x)  is-one-ℕ d  quotient-div-ℕ d x H  x
compute-quotient-div-is-one-ℕ .1 x (u , q) refl =
  inv (right-unit-law-mul-ℕ u)  q

is-one-divisor-ℕ :
  (d x : )  is-nonzero-ℕ x  (H : div-ℕ d x) 
  quotient-div-ℕ d x H  x  is-one-ℕ d
is-one-divisor-ℕ d x f (.x , q) refl =
  is-injective-left-mul-ℕ x f (q  inv (right-unit-law-mul-ℕ x))
```

### If `x` is nonzero and `d | x` is a nontrivial divisor, then `x/d < x`

```agda
le-quotient-div-ℕ :
  (d x : )  is-nonzero-ℕ x  (H : div-ℕ d x)  ¬ (is-one-ℕ d) 
  le-ℕ (quotient-div-ℕ d x H) x
le-quotient-div-ℕ d x f H g =
  map-left-unit-law-coproduct-is-empty
    ( quotient-div-ℕ d x H  x)
    ( le-ℕ (quotient-div-ℕ d x H) x)
    ( map-neg (is-one-divisor-ℕ d x f H) g)
    ( eq-or-le-leq-ℕ
      ( quotient-div-ℕ d x H)
      ( x)
      ( leq-quotient-div-ℕ d x f H))
```