Bezout's lemma on the natural numbers

Content created by Fredrik Bakke, Egbert Rijke, Victor Blanchi, Jonathan Prieto-Cubides and malarbol.

Created on 2023-04-08.
Last modified on 2024-03-28.

module elementary-number-theory.bezouts-lemma-natural-numbers where
Imports
open import elementary-number-theory.absolute-value-integers
open import elementary-number-theory.addition-integers
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.congruence-integers
open import elementary-number-theory.distance-integers
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.divisibility-modular-arithmetic
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.euclidean-division-natural-numbers
open import elementary-number-theory.greatest-common-divisor-natural-numbers
open import elementary-number-theory.inequality-integers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.integers
open import elementary-number-theory.lower-bounds-natural-numbers
open import elementary-number-theory.modular-arithmetic
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.multiplication-positive-and-negative-integers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.nonnegative-integers
open import elementary-number-theory.positive-and-negative-integers
open import elementary-number-theory.strict-inequality-natural-numbers
open import elementary-number-theory.well-ordering-principle-natural-numbers

open import foundation.action-on-identifications-functions
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.identity-types
open import foundation.negation
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types

Idea

Bezout's lemma shows that for any two natural numbers x and y there exist k and l such that dist-ℕ (kx,ly) = gcd(x,y). To prove this, note that the predicate P : ℕ → UU lzero given by

  P z := Σ (k : ℕ), Σ (l : ℕ), dist-ℕ (kx, ly) = z

is decidable, because P z ⇔ [y]_x | [z]_x in ℤ/x. The least positive z such that P z holds is gcd x y.

Definitions

is-distance-between-multiples-ℕ :       UU lzero
is-distance-between-multiples-ℕ x y z =
  Σ   k  Σ   l  dist-ℕ (k *ℕ x) (l *ℕ y)  z))

is-distance-between-multiples-fst-coeff-ℕ :
  {x y z : }  is-distance-between-multiples-ℕ x y z  
is-distance-between-multiples-fst-coeff-ℕ dist = pr1 dist

is-distance-between-multiples-snd-coeff-ℕ :
  {x y z : }  is-distance-between-multiples-ℕ x y z  
is-distance-between-multiples-snd-coeff-ℕ dist = pr1 (pr2 dist)

is-distance-between-multiples-eqn-ℕ :
  {x y z : } (d : is-distance-between-multiples-ℕ x y z) 
  dist-ℕ
    ( (is-distance-between-multiples-fst-coeff-ℕ d) *ℕ x)
    ( (is-distance-between-multiples-snd-coeff-ℕ d) *ℕ y)  z
is-distance-between-multiples-eqn-ℕ dist = pr2 (pr2 dist)

is-distance-between-multiples-sym-ℕ :
  (x y z : )  is-distance-between-multiples-ℕ x y z 
  is-distance-between-multiples-ℕ y x z
is-distance-between-multiples-sym-ℕ x y z (pair k (pair l eqn)) =
  pair l (pair k (symmetric-dist-ℕ (l *ℕ y) (k *ℕ x)  eqn))

Lemmas

If z = dist-ℕ (kx, ly) for some k and l, then [y] | [z] in ℤ-Mod x

If z = dist-ℕ (kx, ly) for some k and l, then it follows that ly ≡ ±z mod x. It follows that ±ly ≡ z mod x, and therefore that [y] | [z] in ℤ-Mod x

int-is-distance-between-multiples-ℕ :
  (x y z : ) (d : is-distance-between-multiples-ℕ x y z) 
  ( H :
    leq-ℕ
      ( (is-distance-between-multiples-fst-coeff-ℕ d) *ℕ x)
      ( (is-distance-between-multiples-snd-coeff-ℕ d) *ℕ y)) 
  ( int-ℕ z) +ℤ
  ( (int-ℕ (is-distance-between-multiples-fst-coeff-ℕ d)) *ℤ (int-ℕ x)) 
  ( int-ℕ (is-distance-between-multiples-snd-coeff-ℕ d)) *ℤ (int-ℕ y)
int-is-distance-between-multiples-ℕ x y z (k , l , p) H =
  equational-reasoning
    (int-ℕ z) +ℤ ((int-ℕ k) *ℤ (int-ℕ x))
     (int-ℕ z) +ℤ (int-ℕ (k *ℕ x))
      by ap ((int-ℕ z) +ℤ_) (mul-int-ℕ k x)
     int-ℕ (z +ℕ (k *ℕ x))
      by add-int-ℕ z (k *ℕ x)
     int-ℕ (l *ℕ y)
      by ap (int-ℕ) (rewrite-left-dist-add-ℕ z (k *ℕ x) (l *ℕ y) H (inv p))
     (int-ℕ l) *ℤ (int-ℕ y)
      by inv (mul-int-ℕ l y)

div-mod-is-distance-between-multiples-ℕ :
  (x y z : ) 
  is-distance-between-multiples-ℕ x y z  div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z)
div-mod-is-distance-between-multiples-ℕ x y z (k , l , p) =
  kxly-case-split (linear-leq-ℕ (k *ℕ x) (l *ℕ y))
  where
  kxly-case-split :
    leq-ℕ (k *ℕ x) (l *ℕ y) + leq-ℕ (l *ℕ y) (k *ℕ x) 
    div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z)
  kxly-case-split (inl kxly) =
    ( mod-ℕ x l ,
      ( equational-reasoning
        mul-ℤ-Mod x (mod-ℕ x l) (mod-ℕ x y)
         mul-ℤ-Mod x (mod-ℤ x (int-ℕ l)) (mod-ℕ x y)
          by inv (ap  p  mul-ℤ-Mod x p (mod-ℕ x y)) (mod-int-ℕ x l))
         mul-ℤ-Mod x (mod-ℤ x (int-ℕ l)) (mod-ℤ x (int-ℕ y))
          by inv (ap  p  mul-ℤ-Mod x (mod-ℤ x (int-ℕ l)) p) (mod-int-ℕ x y))
         mod-ℤ x ((int-ℕ l) *ℤ (int-ℕ y))
          by inv (preserves-mul-mod-ℤ x (int-ℕ l) (int-ℕ y))
         mod-ℤ x ((int-ℕ z) +ℤ ((int-ℕ k) *ℤ (int-ℕ x)))
          by
          inv
            ( ap
              ( mod-ℤ x)
              ( int-is-distance-between-multiples-ℕ x y z (k , l , p) kxly))
         add-ℤ-Mod x (mod-ℤ x (int-ℕ z)) (mod-ℤ x ((int-ℕ k) *ℤ (int-ℕ x)))
          by preserves-add-mod-ℤ x (int-ℕ z) ((int-ℕ k) *ℤ (int-ℕ x))
         add-ℤ-Mod x
            ( mod-ℤ x (int-ℕ z))
            ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) (mod-ℤ x (int-ℕ x)))
          by
          ap
            ( add-ℤ-Mod x (mod-ℤ x (int-ℕ z)))
            ( preserves-mul-mod-ℤ x (int-ℕ k) (int-ℕ x))
         add-ℤ-Mod x
            ( mod-ℤ x (int-ℕ z))
            ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) (mod-ℤ x zero-ℤ))
          by
          ap
            ( λ p 
              add-ℤ-Mod x
                ( mod-ℤ x (int-ℕ z))
                ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) p))
            ( mod-int-ℕ x x  (mod-refl-ℕ x  inv (mod-zero-ℤ x)))
         add-ℤ-Mod x
            ( mod-ℤ x (int-ℕ z))
            ( mod-ℤ x ((int-ℕ k) *ℤ zero-ℤ))
          by
          ap
            ( add-ℤ-Mod x (mod-ℤ x (int-ℕ z)))
            ( inv (preserves-mul-mod-ℤ x (int-ℕ k) zero-ℤ))
         add-ℤ-Mod x (mod-ℤ x (int-ℕ z)) (mod-ℤ x zero-ℤ)
          by
          ap
            ( λ p  add-ℤ-Mod x (mod-ℤ x (int-ℕ z)) (mod-ℤ x p))
            ( right-zero-law-mul-ℤ (int-ℕ k))
         mod-ℤ x ((int-ℕ z) +ℤ zero-ℤ)
          by inv (preserves-add-mod-ℤ x (int-ℕ z) zero-ℤ)
         mod-ℤ x (int-ℕ z)
          by ap (mod-ℤ x) (right-unit-law-add-ℤ (int-ℕ z))
         mod-ℕ x z by mod-int-ℕ x z))
  kxly-case-split (inr lykx) =
    ( mod-ℤ x (neg-ℤ (int-ℕ l)) ,
      ( equational-reasoning
        mul-ℤ-Mod x (mod-ℤ x (neg-ℤ (int-ℕ l))) (mod-ℕ x y)
         mul-ℤ-Mod x (mod-ℤ x (neg-ℤ (int-ℕ l))) (mod-ℤ x (int-ℕ y))
          by
          inv
            ( ap
              ( mul-ℤ-Mod x (mod-ℤ x (neg-ℤ (int-ℕ l))))
              ( mod-int-ℕ x y))
         mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))
          by inv (preserves-mul-mod-ℤ x (neg-ℤ (int-ℕ l)) (int-ℕ y))
         mod-ℤ x (((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) +ℤ zero-ℤ)
          by
          ap
            ( mod-ℤ x)
            ( inv (right-unit-law-add-ℤ ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))
         add-ℤ-Mod x
            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
            ( mod-ℤ x zero-ℤ)
          by preserves-add-mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) (zero-ℤ)
         add-ℤ-Mod x
            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
            ( mod-ℤ x ((int-ℕ k) *ℤ zero-ℤ))
          by
          ap
            ( λ p 
              add-ℤ-Mod x
                ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
                ( mod-ℤ x p))
            ( inv (right-zero-law-mul-ℤ (int-ℕ k)))
         add-ℤ-Mod x
            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
            ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) (mod-ℤ x zero-ℤ))
          by
          ap
            ( add-ℤ-Mod x (mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))
            ( preserves-mul-mod-ℤ x (int-ℕ k) zero-ℤ)
         add-ℤ-Mod x
            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
            ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) (mod-ℤ x (int-ℕ x)))
          by
          ap
            ( λ p 
              add-ℤ-Mod x
                ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
                ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) p))
            ( mod-zero-ℤ x  (inv (mod-refl-ℕ x)  inv (mod-int-ℕ x x)))
         add-ℤ-Mod x
            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
            ( mod-ℤ x ((int-ℕ k) *ℤ (int-ℕ x)))
          by
          ap
            ( add-ℤ-Mod x (mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))
            ( inv (preserves-mul-mod-ℤ x (int-ℕ k) (int-ℕ x)))
         mod-ℤ x
            ( ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) +ℤ ((int-ℕ k) *ℤ (int-ℕ x)))
          by
          inv
            ( preserves-add-mod-ℤ x
              ( (neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))
              ( (int-ℕ k) *ℤ (int-ℕ x)))
         mod-ℤ x (int-ℕ z)
          by
          ap
            ( mod-ℤ x)
            ( equational-reasoning
              ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) +ℤ ((int-ℕ k) *ℤ (int-ℕ x))
               (neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y))) +ℤ ((int-ℕ k) *ℤ (int-ℕ x))
                by
                ap
                  ( _+ℤ ((int-ℕ k) *ℤ (int-ℕ x)))
                  ( left-negative-law-mul-ℤ (int-ℕ l) (int-ℕ y))
               ((int-ℕ k) *ℤ (int-ℕ x)) +ℤ (neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
                by
                commutative-add-ℤ
                  ( neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
                  ( (int-ℕ k) *ℤ (int-ℕ x))
               add-ℤ
                  ( (int-ℕ z) +ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
                  ( neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
                by
                ap
                  ( _+ℤ (neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y))))
                  ( inv
                    ( int-is-distance-between-multiples-ℕ y x z
                      ( is-distance-between-multiples-sym-ℕ x y z (k , l , p))
                    ( lykx)))
               int-ℕ z
                by
                is-retraction-right-add-neg-ℤ
                  ( (int-ℕ l) *ℤ (int-ℕ y))
                  ( int-ℕ z))
               mod-ℕ x z by mod-int-ℕ x z))

If [y] | [z] in ℤ-Mod x, then z = dist-ℕ (kx, ly) for some k and l

If x = 0, then we can simply argue in . Otherwise, if [y] | [z] in ℤ-Mod x, there exists some equivalence class u in ℤ-Mod x such that [u] [y] ≡ [z] as a congruence mod x. This u can always be chosen such that x > u ≥ 0. Therefore, there exists some integer a ≥ 0 such that ax = uy - z, or ax = z - uy. In the first case, we can extract the distance condition we desire. In the other case, we have that ax + uy = z. This can be written as (a + y)x + (u - x)y = z, so that the second term is nonpositive. Then, in this case, we again can extract the distance condition we desire.

cong-div-mod-ℤ :
  (x y z : ) (q : div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z)) 
  cong-ℤ (int-ℕ x) ((int-ℤ-Mod x (pr1 q)) *ℤ (int-ℕ y)) (int-ℕ z)
cong-div-mod-ℤ x y z (u , p) =
  cong-eq-mod-ℤ x
    ( (int-ℤ-Mod x u) *ℤ (int-ℕ y))
    ( int-ℕ z)
    ( equational-reasoning
      mod-ℤ x ((int-ℤ-Mod x u) *ℤ (int-ℕ y))
       mul-ℤ-Mod x (mod-ℤ x (int-ℤ-Mod x u)) (mod-ℤ x (int-ℕ y))
        by preserves-mul-mod-ℤ x (int-ℤ-Mod x u) (int-ℕ y)
       mul-ℤ-Mod x u (mod-ℤ x (int-ℕ y))
        by
        ap
          ( λ p  mul-ℤ-Mod x p (mod-ℤ x (int-ℕ y)))
          ( is-section-int-ℤ-Mod x u)
       mul-ℤ-Mod x u (mod-ℕ x y)
        by ap (mul-ℤ-Mod x u) (mod-int-ℕ x y)
       mod-ℕ x z by p
       mod-ℤ x (int-ℕ z) by inv (mod-int-ℕ x z))

is-distance-between-multiples-div-mod-ℕ :
  (x y z : ) 
  div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z)  is-distance-between-multiples-ℕ x y z
is-distance-between-multiples-div-mod-ℕ zero-ℕ y z (u , p) =
  u-nonneg-case-split (decide-is-nonnegative-is-nonnegative-neg-ℤ {u})
  where
  u-nonneg-case-split :
    (is-nonnegative-ℤ u + is-nonnegative-ℤ (neg-ℤ u)) 
    is-distance-between-multiples-ℕ zero-ℕ y z
  u-nonneg-case-split (inl nonneg) =
    ( zero-ℕ ,
      abs-ℤ u ,
      is-injective-int-ℕ
        ( inv (mul-int-ℕ (abs-ℤ u) y) 
          ( ( ap
              ( _*ℤ (int-ℕ y))
              ( int-abs-is-nonnegative-ℤ u nonneg)) 
            ( p))))
  u-nonneg-case-split (inr neg) =
    ( zero-ℕ ,
      zero-ℕ ,
      is-injective-int-ℕ
        ( inv
          ( is-zero-is-nonnegative-neg-is-nonnegative-ℤ
            ( is-nonnegative-int-ℕ z)
            ( tr
              ( is-nonnegative-ℤ)
              ( left-negative-law-mul-ℤ u (int-ℕ y)  ap (neg-ℤ) p)
              ( is-nonnegative-mul-ℤ neg (is-nonnegative-int-ℕ y))))))

is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
  uy-z-case-split (decide-is-nonnegative-is-nonnegative-neg-ℤ
    { ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z))})
  where
  a : 
  a = pr1 (cong-div-mod-ℤ (succ-ℕ x) y z (u , p))

  a-eqn-pos :
    add-ℤ
      ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
      ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x)))) 
    int-ℕ z
  a-eqn-pos =
    equational-reasoning
    add-ℤ
      ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
      ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
     add-ℤ
        ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
      by
      commutative-add-ℤ
        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
        ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
     add-ℤ
        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
      by
      ap
        ( _+ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
        ( inv (left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x))))
     add-ℤ
        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
        ( add-ℤ
          ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z)))
          ( int-ℕ z))
      by
      ap
        ( ((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
        ( inv
          ( is-section-right-add-neg-ℤ
            ( int-ℕ z)
            ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))))
     add-ℤ
        ( add-ℤ
          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
          ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z))))
        ( int-ℕ z)
      by
      inv
        ( associative-add-ℤ
          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
          ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z)))
          ( int-ℕ z))
     add-ℤ
        ( add-ℤ
          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
          ( a *ℤ (int-ℕ (succ-ℕ x))))
        ( int-ℕ z)
      by
      ap
        ( λ p  (((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ p) +ℤ (int-ℕ z))
        ( inv (pr2 (cong-div-mod-ℤ (succ-ℕ x) y z (u , p))))
     add-ℤ
        ( add-ℤ
          ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
          ( a *ℤ (int-ℕ (succ-ℕ x))))
        ( int-ℕ z)
      by
      ap
        ( λ p  (p +ℤ (a *ℤ (int-ℕ (succ-ℕ x)))) +ℤ (int-ℕ z))
        ( left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x)))
     zero-ℤ +ℤ (int-ℕ z)
      by
      ap
        ( _+ℤ (int-ℕ z))
        ( left-inverse-law-add-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
     int-ℕ z by left-unit-law-add-ℤ (int-ℕ z)

  a-extra-eqn-neg :
    add-ℤ
      ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
      ( neg-ℤ
        ( mul-ℤ
          ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
          ( int-ℕ y))) 
    ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ int-ℕ y) +ℤ (neg-ℤ (a *ℤ int-ℕ (succ-ℕ x)))
  a-extra-eqn-neg =
    equational-reasoning
    add-ℤ
      ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
      ( neg-ℤ
        ( mul-ℤ
          ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
          ( int-ℕ y)))
     add-ℤ
        ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
        ( mul-ℤ
          ( neg-ℤ ((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))))
          ( int-ℕ y))
      by
      ap
        ( (((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
        ( inv
          ( left-negative-law-mul-ℤ
            ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
            ( int-ℕ y)))
     add-ℤ
        ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
        ( ((int-ℤ-Mod (succ-ℕ x) u) +ℤ (neg-ℤ (int-ℕ (succ-ℕ x)))) *ℤ (int-ℕ y))
      by
      ap
        ( λ p 
          add-ℤ
            ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
            ( p *ℤ (int-ℕ y)))
        ( equational-reasoning
          neg-ℤ ((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
           neg-ℤ ((neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)) +ℤ (int-ℕ (succ-ℕ x)))
            by
            ap
              ( neg-ℤ)
              ( commutative-add-ℤ
                ( int-ℕ (succ-ℕ x))
                ( neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
           add-ℤ
              ( neg-ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
              ( neg-ℤ (int-ℕ (succ-ℕ x)))
            by
            distributive-neg-add-ℤ
              ( neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))
              ( int-ℕ (succ-ℕ x))
           (int-ℤ-Mod (succ-ℕ x) u) +ℤ (neg-ℤ (int-ℕ (succ-ℕ x)))
            by
            ap
              ( _+ℤ (neg-ℤ (int-ℕ (succ-ℕ x))))
              ( neg-neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
     add-ℤ
        ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
        ( add-ℤ
          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
          ( (neg-ℤ (int-ℕ (succ-ℕ x))) *ℤ (int-ℕ y)))
      by
      ap
        ( (((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
        ( right-distributive-mul-add-ℤ
          ( int-ℤ-Mod (succ-ℕ x) u)
          ( neg-ℤ (int-ℕ (succ-ℕ x)))
          ( int-ℕ y))
     add-ℤ
        ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
        ( add-ℤ
          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))))
      by
      ap
        ( λ p 
          add-ℤ
            ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
            ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ p))
        ( left-negative-law-mul-ℤ (int-ℕ (succ-ℕ x)) (int-ℕ y))
     add-ℤ
        ( add-ℤ
          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
          ( (int-ℕ y) *ℤ (int-ℕ (succ-ℕ x))))
        ( add-ℤ
          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))))
      by
      ap
        ( _+ℤ
          ( add-ℤ
            ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
            ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))))
        ( right-distributive-mul-add-ℤ (neg-ℤ a) (int-ℕ y) (int-ℕ (succ-ℕ x)))
     add-ℤ
        ( add-ℤ
          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
          ( (int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))
        ( add-ℤ
          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))))
      by
      ap
        ( λ p 
          add-ℤ
            ( ((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ p)
            ( add-ℤ
              ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
              ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))))
        ( commutative-mul-ℤ (int-ℕ y) (int-ℕ (succ-ℕ x)))
     add-ℤ
        ( add-ℤ
          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
        ( add-ℤ
          ( (int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))
          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))))
      by
      interchange-law-add-add-ℤ
        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
        ( (int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))
        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
        ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))
     add-ℤ
        ( add-ℤ
          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
        ( zero-ℤ)
      by
      ap
        ( add-ℤ
          ( add-ℤ
            ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
            ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))))
          ( right-inverse-law-add-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))
     add-ℤ
        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
      by
      right-unit-law-add-ℤ
        ( add-ℤ
          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
     add-ℤ
        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
      by
      commutative-add-ℤ
        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
     add-ℤ
        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
        ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
      by
      ap
        ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ_)
        ( left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x)))

  uy-z-case-split :
    ( ( is-nonnegative-ℤ
        ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z)))) +
      ( is-nonnegative-ℤ
        ( neg-ℤ
          ( add-ℤ
            ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
            ( neg-ℤ (int-ℕ z)))))) 
    is-distance-between-multiples-ℕ (succ-ℕ x) y z
  uy-z-case-split (inl uy-z) =
    ( abs-ℤ a ,
      nat-Fin (succ-ℕ x) u ,
      ( equational-reasoning
        dist-ℕ ((abs-ℤ a) *ℕ (succ-ℕ x)) ((nat-Fin (succ-ℕ x) u) *ℕ y)
         dist-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y) ((abs-ℤ a) *ℕ (succ-ℕ x))
          by
          symmetric-dist-ℕ
            ( (abs-ℤ a) *ℕ (succ-ℕ x))
            ( (nat-Fin (succ-ℕ x) u) *ℕ y)
         dist-ℤ
            ( int-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y))
            ( int-ℕ ((abs-ℤ a) *ℕ (succ-ℕ x)))
          by
          inv
            ( dist-int-ℕ
              ( (nat-Fin (succ-ℕ x) u) *ℕ y)
              ( (abs-ℤ a) *ℕ (succ-ℕ x)))
         dist-ℤ
            ( int-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y))
            ( (int-ℕ (abs-ℤ a)) *ℤ (int-ℕ (succ-ℕ x)))
          by
          ap
            ( dist-ℤ (int-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y)))
            ( inv (mul-int-ℕ (abs-ℤ a) (succ-ℕ x)))
         dist-ℤ
            ( (int-ℕ (nat-Fin (succ-ℕ x) u)) *ℤ (int-ℕ y))
            ( (int-ℕ (abs-ℤ a)) *ℤ (int-ℕ (succ-ℕ x)))
          by
          ap
            ( λ p  dist-ℤ p ((int-ℕ (abs-ℤ a)) *ℤ (int-ℕ (succ-ℕ x))))
            ( inv (mul-int-ℕ (nat-Fin (succ-ℕ x) u) y))
         dist-ℤ
            ( (int-ℕ (nat-Fin (succ-ℕ x) u)) *ℤ (int-ℕ y))
            ( a *ℤ (int-ℕ (succ-ℕ x)))
          by
          ap
            ( λ p 
              dist-ℤ
                ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
                ( p *ℤ (int-ℕ (succ-ℕ x))))
            ( int-abs-is-nonnegative-ℤ a a-is-nonnegative-ℤ)
         abs-ℤ (int-ℕ z)
          by ap (abs-ℤ) a-eqn-pos
         z
          by abs-int-ℕ z))
    where
    a-is-nonnegative-ℤ : is-nonnegative-ℤ a
    a-is-nonnegative-ℤ =
      is-nonnegative-left-factor-mul-ℤ
        ( tr
          ( is-nonnegative-ℤ)
          ( inv
            ( pr2 (cong-div-mod-ℤ (succ-ℕ x) y z (u , p))))
          ( uy-z))
        ( is-nonnegative-int-ℕ (succ-ℕ x))

  uy-z-case-split (inr z-uy) =
    ( (abs-ℤ a) +ℕ y ,
      abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) ,
      ( equational-reasoning
        dist-ℕ (((abs-ℤ a) +ℕ y) *ℕ (succ-ℕ x))
          (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y)
         dist-ℤ (int-ℕ (((abs-ℤ a) +ℕ y) *ℕ (succ-ℕ x)))
          (int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
        by inv (dist-int-ℕ (((abs-ℤ a) +ℕ y) *ℕ (succ-ℕ x))
          (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
         dist-ℤ ((int-ℕ ((abs-ℤ a) +ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
          (int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
        by ap  p  dist-ℤ p (int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y)))
          (inv (mul-int-ℕ ((abs-ℤ a) +ℕ y) (succ-ℕ x)))
         dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
          (int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
        by
          ap
            ( λ p 
              dist-ℤ
                ( p *ℤ (int-ℕ (succ-ℕ x)))
                ( int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
                  (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y)))
          (inv (add-int-ℕ (abs-ℤ a) y))
         dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
          (mul-ℤ (int-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))))) (int-ℕ y))
        by
          ap
            ( dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x))))
            ( inv (mul-int-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
              (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
         dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
          (mul-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
            (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) (int-ℕ y))
          by ap  p  dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ
              (int-ℕ (succ-ℕ x))) (p *ℤ (int-ℕ y)))
          (int-abs-is-nonnegative-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
            (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) (int-ℤ-Mod-bounded x u))
         dist-ℤ
            ( ((int-ℕ (abs-ℤ (neg-ℤ a))) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
            ( mul-ℤ
              ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
              ( int-ℕ y))
        by
          ap
            ( λ p 
              dist-ℤ
                ( ((int-ℕ p) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
                ( mul-ℤ
                  ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
                  ( int-ℕ y)))
          (inv (abs-neg-ℤ a))
         dist-ℤ (((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
          (mul-ℤ
            ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) (int-ℕ y))
        by ap  p  dist-ℤ ((p +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
          (((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) *ℤ
            (int-ℕ y)))
          (int-abs-is-nonnegative-ℤ (neg-ℤ a) neg-a-is-nonnegative-ℤ)
         abs-ℤ (int-ℕ z)
        by ap abs-ℤ (a-extra-eqn-neg  a-eqn-pos)
         z by abs-int-ℕ z))
    where
    neg-a-is-nonnegative-ℤ : is-nonnegative-ℤ (neg-ℤ a)
    neg-a-is-nonnegative-ℤ =
      is-nonnegative-left-factor-mul-ℤ
        ( tr is-nonnegative-ℤ
          ( equational-reasoning
            ( neg-ℤ (((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ
              ( neg-ℤ (int-ℕ z))))
             ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ
                ( neg-ℤ (neg-ℤ (int-ℕ z)))
              by
                ( distributive-neg-add-ℤ
                  ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
                  ( neg-ℤ (int-ℕ z)))
             ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ
                ( int-ℕ z)
              by
                ap
                  ( (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ_)
                  ( neg-neg-ℤ (int-ℕ z))
             add-ℤ
              ( int-ℕ z)
              ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
              by
                commutative-add-ℤ
                  ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
                  ( int-ℕ z)
             (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))
              by inv (pr2
                ( symmetric-cong-ℤ (int-ℕ (succ-ℕ x))
                ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) (int-ℕ z)
                ( cong-div-mod-ℤ (succ-ℕ x) y z (u , p)))))
          ( z-uy))
          ( is-nonnegative-int-ℕ (succ-ℕ x))

The type is-distance-between-multiples-ℕ x y z is decidable

is-decidable-is-distance-between-multiples-ℕ :
  (x y z : )  is-decidable (is-distance-between-multiples-ℕ x y z)
is-decidable-is-distance-between-multiples-ℕ x y z =
  decidable-div-ℤ-case-split
    (is-decidable-div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z))
  where
  decidable-div-ℤ-case-split :
    ( div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z) +
      ¬ ( div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z))) 
    is-decidable (is-distance-between-multiples-ℕ x y z)
  decidable-div-ℤ-case-split (inl div-Mod) =
    inl (is-distance-between-multiples-div-mod-ℕ x y z div-Mod)
  decidable-div-ℤ-case-split (inr neg-div-Mod) =
    inr  dist  neg-div-Mod
      (div-mod-is-distance-between-multiples-ℕ x y z dist))

Theorem

Since is-distance-between-multiples-ℕ x y z is decidable, we can prove Bezout's lemma by the well-ordering principle. First, take the least positive distance d between multiples of x and y.

pos-distance-between-multiples : (x y z : )  UU lzero
pos-distance-between-multiples x y z = is-nonzero-ℕ (x +ℕ y) 
  (is-nonzero-ℕ z) × (is-distance-between-multiples-ℕ x y z)

is-inhabited-pos-distance-between-multiples :
  (x y : )  Σ  (pos-distance-between-multiples x y)
is-inhabited-pos-distance-between-multiples zero-ℕ zero-ℕ =
  pair zero-ℕ  H  ex-falso (H refl))
is-inhabited-pos-distance-between-multiples zero-ℕ (succ-ℕ y) =
  pair (succ-ℕ y)  H  pair' (is-nonzero-succ-ℕ y)
    (pair zero-ℕ (pair 1 (ap succ-ℕ (left-unit-law-add-ℕ y)))))
is-inhabited-pos-distance-between-multiples (succ-ℕ x) y = pair (succ-ℕ x)
   H  pair' (is-nonzero-succ-ℕ x)
    (pair 1 (pair zero-ℕ (ap succ-ℕ (left-unit-law-add-ℕ x)))))

minimal-pos-distance-between-multiples :
  (x y : )  minimal-element-ℕ (pos-distance-between-multiples x y)
minimal-pos-distance-between-multiples x y = well-ordering-principle-ℕ
  (pos-distance-between-multiples x y)
   z  is-decidable-function-type
    (is-decidable-neg (is-decidable-is-zero-ℕ (x +ℕ y)))
    (is-decidable-product (is-decidable-neg (is-decidable-is-zero-ℕ z))
      (is-decidable-is-distance-between-multiples-ℕ x y z)))
  (is-inhabited-pos-distance-between-multiples x y)

minimal-positive-distance : (x y : )  
minimal-positive-distance x y = pr1 (minimal-pos-distance-between-multiples x y)

Then d divides both x and y. Since gcd x y divides any number of the form dist-ℕ (kx,ly), it follows that gcd x y | d, and hence that gcd x y = d.

minimal-positive-distance-is-distance :
  (x y : )  is-nonzero-ℕ (x +ℕ y) 
  (is-distance-between-multiples-ℕ x y (minimal-positive-distance x y))
minimal-positive-distance-is-distance x y nonzero =
  pr2 ((pr1 (pr2 (minimal-pos-distance-between-multiples x y))) nonzero)

minimal-positive-distance-is-minimal :
  (x y : ) 
  is-lower-bound-ℕ
    ( pos-distance-between-multiples x y)
    ( minimal-positive-distance x y)
minimal-positive-distance-is-minimal x y =
  pr2 (pr2 (minimal-pos-distance-between-multiples x y))

minimal-positive-distance-nonzero :
  (x y : ) 
  (is-nonzero-ℕ (x +ℕ y)) 
  (is-nonzero-ℕ (minimal-positive-distance x y))
minimal-positive-distance-nonzero x y nonzero =
  pr1 ((pr1 (pr2 (minimal-pos-distance-between-multiples x y))) nonzero)

minimal-positive-distance-leq-sym :
  (x y : ) 
  leq-ℕ (minimal-positive-distance x y) (minimal-positive-distance y x)
minimal-positive-distance-leq-sym x y =
  minimal-positive-distance-is-minimal x y (minimal-positive-distance y x)
   H 
    pair'
      ( minimal-positive-distance-nonzero
        ( y)
        ( x)
        ( λ K  H (commutative-add-ℕ x y  K)))
      ( is-distance-between-multiples-sym-ℕ
        ( y)
        ( x)
        ( minimal-positive-distance y x)
        ( minimal-positive-distance-is-distance
          ( y)
          ( x)
          ( λ K  H (commutative-add-ℕ x y  K)))))

minimal-positive-distance-sym :
  (x y : )  minimal-positive-distance x y  minimal-positive-distance y x
minimal-positive-distance-sym x y = antisymmetric-leq-ℕ
  (minimal-positive-distance x y)
  (minimal-positive-distance y x)
  (minimal-positive-distance-leq-sym x y)
  (minimal-positive-distance-leq-sym y x)

minimal-positive-distance-x-coeff : (x y : )  (is-nonzero-ℕ (x +ℕ y))  
minimal-positive-distance-x-coeff x y H =
  pr1 (minimal-positive-distance-is-distance x y H)

minimal-positive-distance-succ-x-coeff : (x y : )  
minimal-positive-distance-succ-x-coeff x y =
  minimal-positive-distance-x-coeff
    ( succ-ℕ x)
    ( y)
    ( tr
      ( is-nonzero-ℕ)
      ( inv (left-successor-law-add-ℕ x y))
      ( is-nonzero-succ-ℕ (x +ℕ y)))

minimal-positive-distance-y-coeff : (x y : )  (is-nonzero-ℕ (x +ℕ y))  
minimal-positive-distance-y-coeff x y H =
  pr1 (pr2 (minimal-positive-distance-is-distance x y H))

minimal-positive-distance-succ-y-coeff : (x y : )  
minimal-positive-distance-succ-y-coeff x y =
  minimal-positive-distance-y-coeff
    ( succ-ℕ x)
    ( y)
    ( tr
      ( is-nonzero-ℕ)
      ( inv (left-successor-law-add-ℕ x y))
      ( is-nonzero-succ-ℕ (x +ℕ y)))

minimal-positive-distance-eqn :
  (x y : ) (H : is-nonzero-ℕ (x +ℕ y)) 
  dist-ℕ
    ( (minimal-positive-distance-x-coeff x y H) *ℕ x)
    ( (minimal-positive-distance-y-coeff x y H) *ℕ y) 
  minimal-positive-distance x y
minimal-positive-distance-eqn x y H =
  pr2 (pr2 (minimal-positive-distance-is-distance x y H))

minimal-positive-distance-succ-eqn :
  (x y : ) 
  dist-ℕ
    ( (minimal-positive-distance-succ-x-coeff x y) *ℕ (succ-ℕ x))
    ( (minimal-positive-distance-succ-y-coeff x y) *ℕ y) 
  minimal-positive-distance (succ-ℕ x) y
minimal-positive-distance-succ-eqn x y =
  minimal-positive-distance-eqn
    ( succ-ℕ x)
    ( y)
    ( tr
      ( is-nonzero-ℕ)
      ( inv (left-successor-law-add-ℕ x y))
      ( is-nonzero-succ-ℕ (x +ℕ y)))

minimal-positive-distance-div-succ-x-eqn :
  (x y : ) 
  add-ℤ
    ( mul-ℤ
      ( int-ℕ
        ( quotient-euclidean-division-ℕ
          ( minimal-positive-distance (succ-ℕ x) y)
          ( succ-ℕ x)))
      ( int-ℕ (minimal-positive-distance (succ-ℕ x) y)))
    ( int-ℕ
      ( remainder-euclidean-division-ℕ
        ( minimal-positive-distance (succ-ℕ x) y)
        ( succ-ℕ x))) 
      int-ℕ (succ-ℕ x)
minimal-positive-distance-div-succ-x-eqn x y =
    equational-reasoning
      add-ℤ
        ( mul-ℤ
          ( int-ℕ
            ( quotient-euclidean-division-ℕ
              ( minimal-positive-distance (succ-ℕ x) y)
              ( succ-ℕ x)))
          ( int-ℕ (minimal-positive-distance (succ-ℕ x) y)))
        ( int-ℕ
          ( remainder-euclidean-division-ℕ
            ( minimal-positive-distance (succ-ℕ x) y)
            ( succ-ℕ x)))
       add-ℤ
          ( int-ℕ
            ( mul-ℕ
              ( quotient-euclidean-division-ℕ
                ( minimal-positive-distance (succ-ℕ x) y)
                ( succ-ℕ x))
              ( minimal-positive-distance (succ-ℕ x) y)))
          ( int-ℕ
            ( remainder-euclidean-division-ℕ
              ( minimal-positive-distance (succ-ℕ x) y)
              ( succ-ℕ x)))
          by
            ( ap
              ( _+ℤ
                ( int-ℕ
                  ( remainder-euclidean-division-ℕ
                    ( minimal-positive-distance (succ-ℕ x) y)
                    ( succ-ℕ x))))
              ( mul-int-ℕ
                ( quotient-euclidean-division-ℕ
                  ( minimal-positive-distance (succ-ℕ x) y)
                  ( succ-ℕ x))
                ( minimal-positive-distance (succ-ℕ x) y)))
       int-ℕ
            ( add-ℕ
              ( mul-ℕ
                ( quotient-euclidean-division-ℕ
                  ( minimal-positive-distance (succ-ℕ x) y)
                  ( succ-ℕ x))
                ( minimal-positive-distance (succ-ℕ x) y))
              ( remainder-euclidean-division-ℕ
                ( minimal-positive-distance (succ-ℕ x) y)
                ( succ-ℕ x)))
          by
            ( add-int-ℕ
              ( mul-ℕ
                ( quotient-euclidean-division-ℕ
                  ( minimal-positive-distance (succ-ℕ x) y)
                  ( succ-ℕ x))
                ( minimal-positive-distance (succ-ℕ x) y))
              ( remainder-euclidean-division-ℕ
                ( minimal-positive-distance (succ-ℕ x) y)
                ( succ-ℕ x)))
       int-ℕ (succ-ℕ x)
          by
            ap
              ( int-ℕ)
              ( eq-euclidean-division-ℕ
                ( minimal-positive-distance (succ-ℕ x) y)
                ( succ-ℕ x))

remainder-min-dist-succ-x-le-min-dist :
  (x y : ) 
  le-ℕ
    ( remainder-euclidean-division-ℕ
      ( minimal-positive-distance (succ-ℕ x) y)
      ( succ-ℕ x))
    ( minimal-positive-distance (succ-ℕ x) y)
remainder-min-dist-succ-x-le-min-dist x y =
  strict-upper-bound-remainder-euclidean-division-ℕ
    ( minimal-positive-distance (succ-ℕ x) y)
    ( succ-ℕ x)
    ( minimal-positive-distance-nonzero
      ( succ-ℕ x)
      ( y)
      ( tr
        ( is-nonzero-ℕ)
        ( inv (left-successor-law-add-ℕ x y))
        ( is-nonzero-succ-ℕ (x +ℕ y))))

remainder-min-dist-succ-x-is-distance :
  (x y : ) 
  (is-distance-between-multiples-ℕ
    ( succ-ℕ x)
    ( y)
    ( remainder-euclidean-division-ℕ
      ( minimal-positive-distance (succ-ℕ x) y)
      ( succ-ℕ x)))
remainder-min-dist-succ-x-is-distance x y =
  sx-ty-case-split (linear-leq-ℕ (s *ℕ (succ-ℕ x)) (t *ℕ y))
  where
  d : 
  d = minimal-positive-distance (succ-ℕ x) y

  s : 
  s = minimal-positive-distance-succ-x-coeff x y

  t : 
  t = minimal-positive-distance-succ-y-coeff x y

  q : 
  q = quotient-euclidean-division-ℕ d (succ-ℕ x)

  r : 
  r = remainder-euclidean-division-ℕ d (succ-ℕ x)

  dist-sx-ty-eq-d : dist-ℕ (s *ℕ (succ-ℕ x)) (t *ℕ y)  d
  dist-sx-ty-eq-d = minimal-positive-distance-succ-eqn x y

  sx-ty-case-split :
    ( leq-ℕ (s *ℕ (succ-ℕ x)) (t *ℕ y) +
      leq-ℕ (t *ℕ y) (s *ℕ (succ-ℕ x))) 
    is-distance-between-multiples-ℕ (succ-ℕ x) y r
  sx-ty-case-split (inl sxty) =
    ((q *ℕ s) +ℕ 1 , q *ℕ t , inv (dist-eqn))
    where
    add-dist-eqn :
      int-ℕ d 
      ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
    add-dist-eqn =
      equational-reasoning
        int-ℕ d
         ((int-ℕ d) +ℤ (int-ℕ (s *ℕ (succ-ℕ x)))) +ℤ
          (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
          by
          inv
            ( is-retraction-right-add-neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))) (int-ℕ d))
         (int-ℕ (d +ℕ (s *ℕ (succ-ℕ x)))) +ℤ
          (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
          by
          ap
            ( _+ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
            ( add-int-ℕ d (s *ℕ (succ-ℕ x)))
         (int-ℕ (t *ℕ y)) +ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
          by ap  H  (int-ℕ H) +ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
            (rewrite-left-dist-add-ℕ d (s *ℕ (succ-ℕ x))
              (t *ℕ y) sxty (inv (dist-sx-ty-eq-d)))
         ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
          (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
          by
          ap
            ( _+ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
            ( inv (mul-int-ℕ t y))
         ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
          (neg-ℤ ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))
          by
          ap
            ( λ H  ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ (neg-ℤ H))
            ( inv (mul-int-ℕ s (succ-ℕ x)))
         ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
          ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
          by
          ap
            ( ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ_)
            ( inv (left-negative-law-mul-ℤ (int-ℕ s) (int-ℕ (succ-ℕ x))))

    isolate-rem-eqn :
      int-ℕ r 
      add-ℤ
        ( neg-ℤ
          ( mul-ℤ
            ( int-ℕ q)
            ( add-ℤ
              ( (int-ℕ t) *ℤ (int-ℕ y))
              ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
        ( int-ℕ (succ-ℕ x))
    isolate-rem-eqn =
      equational-reasoning
        int-ℕ r
         add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
            ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
          (add-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
              ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
          (int-ℕ r))
          by inv (is-retraction-left-add-neg-ℤ
            ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
            ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
            (int-ℕ r))
         add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
            ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
          (((int-ℕ q) *ℤ (int-ℕ d)) +ℤ (int-ℕ r))
          by
            ap
              ( λ H 
                add-ℤ
                  ( neg-ℤ
                    ( mul-ℤ
                      ( int-ℕ q)
                      ( add-ℤ
                        ( (int-ℕ t) *ℤ (int-ℕ y))
                        ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
                  ( ((int-ℕ q) *ℤ H) +ℤ (int-ℕ r)))
              ( inv add-dist-eqn)
         add-ℤ
            ( neg-ℤ
              ( mul-ℤ
                ( int-ℕ q)
                ( add-ℤ
                  ( (int-ℕ t) *ℤ (int-ℕ y))
                  ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
            ( int-ℕ (succ-ℕ x))
          by
            ap
              ( add-ℤ
                ( neg-ℤ
                  ( mul-ℤ
                    ( int-ℕ q)
                    ( add-ℤ
                      ( (int-ℕ t) *ℤ (int-ℕ y))
                      ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))))
              ( minimal-positive-distance-div-succ-x-eqn x y)

    rearrange-arith-eqn :
      add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
        ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))) (int-ℕ (succ-ℕ x))
       add-ℤ ((((int-ℕ q) *ℤ (int-ℕ s)) +ℤ one-ℤ) *ℤ
          (int-ℕ (succ-ℕ x)))
        (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
    rearrange-arith-eqn =
      equational-reasoning
        add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
          ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))) (int-ℕ (succ-ℕ x))
         add-ℤ (neg-ℤ (((int-ℕ q) *ℤ ((int-ℕ t) *ℤ (int-ℕ y))) +ℤ
          ((int-ℕ q) *ℤ ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
            (int-ℕ (succ-ℕ x))
          by (ap  H  (neg-ℤ H) +ℤ (int-ℕ (succ-ℕ x)))
            (left-distributive-mul-add-ℤ (int-ℕ q) ((int-ℕ t) *ℤ (int-ℕ y))
              ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
         add-ℤ (neg-ℤ ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
          ((int-ℕ q) *ℤ ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
            (int-ℕ (succ-ℕ x))
          by (ap  H  add-ℤ (neg-ℤ (H +ℤ (mul-ℤ (int-ℕ q)
            ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))) (int-ℕ (succ-ℕ x)))
              (inv (associative-mul-ℤ (int-ℕ q) (int-ℕ t) (int-ℕ y))))
         add-ℤ (neg-ℤ ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
          (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
            (int-ℕ (succ-ℕ x))
          by
            ap
              ( λ H 
                add-ℤ
                  ( neg-ℤ
                    ( (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ H))
                  ( int-ℕ (succ-ℕ x)))
            ( equational-reasoning
                ((int-ℕ q) *ℤ ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))
                 ((int-ℕ q) *ℤ (neg-ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))
                  by
                    inv
                      ( associative-mul-ℤ
                        ( int-ℕ q)
                        ( neg-ℤ (int-ℕ s))
                        ( int-ℕ (succ-ℕ x)))
                 (neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))
                  by ap (_*ℤ (int-ℕ (succ-ℕ x)))
                  (right-negative-law-mul-ℤ (int-ℕ q) (int-ℕ s))
                 neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
                  by
                    left-negative-law-mul-ℤ
                      ( (int-ℕ q) *ℤ (int-ℕ s))
                      ( int-ℕ (succ-ℕ x)))
         add-ℤ
            ( add-ℤ
              ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
              ( neg-ℤ
                ( neg-ℤ
                  ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
            (int-ℕ (succ-ℕ x))
          by
            ap
              ( _+ℤ (int-ℕ (succ-ℕ x)))
              ( distributive-neg-add-ℤ
                ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
                ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
         add-ℤ
            ( add-ℤ
              ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
              ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))
            ( int-ℕ (succ-ℕ x))
          by
            ap
              ( λ H 
              add-ℤ
                ( (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))) +ℤ H)
                ( int-ℕ (succ-ℕ x)))
              ( neg-neg-ℤ
                ( ((int-ℕ q) *ℤ ((int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))))
         (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))) +ℤ
          ((((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
            (int-ℕ (succ-ℕ x)))
          by associative-add-ℤ
            (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
            (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
            (int-ℕ (succ-ℕ x))
         add-ℤ ((((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
          (int-ℕ (succ-ℕ x)))
          (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
          by commutative-add-ℤ
            (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
            ((((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
            (int-ℕ (succ-ℕ x)))
         add-ℤ
            ( mul-ℤ
              ( ((int-ℕ q) *ℤ (int-ℕ s)) +ℤ one-ℤ)
              ( int-ℕ (succ-ℕ x)))
            ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
          by
            ap
              ( _+ℤ (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))))
              ( ap
                ( (((int-ℕ q) *ℤ ((int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
                ( left-unit-law-mul-ℤ (int-ℕ (succ-ℕ x))) 
                ( inv
                  ( right-distributive-mul-add-ℤ
                    ( (int-ℕ q) *ℤ (int-ℕ s))
                    ( one-ℤ)
                    ( int-ℕ (succ-ℕ x)))))

    dist-eqn :
      r  dist-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)) ((q *ℕ t) *ℕ y)
    dist-eqn =
      equational-reasoning
        r
         abs-ℤ (int-ℕ r)
          by (inv (abs-int-ℕ r))
         dist-ℤ ((((int-ℕ q) *ℤ (int-ℕ s)) +ℤ one-ℤ) *ℤ
            (int-ℕ (succ-ℕ x)))
          (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
          by (ap (abs-ℤ) (isolate-rem-eqn  rearrange-arith-eqn))
         dist-ℤ
            ( ((int-ℕ (q *ℕ s)) +ℤ (int-ℕ 1)) *ℤ (int-ℕ (succ-ℕ x)))
            ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
          by ap  H  dist-ℤ ((H +ℤ (int-ℕ 1)) *ℤ (int-ℕ (succ-ℕ x)))
            (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
            (mul-int-ℕ q s)
         dist-ℤ ((int-ℕ ((q *ℕ s) +ℕ 1)) *ℤ (int-ℕ (succ-ℕ x)))
          (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
          by ap  H  dist-ℤ (H *ℤ (int-ℕ (succ-ℕ x)))
            (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
            (add-int-ℕ (q *ℕ s) 1)
         dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)))
          (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
          by ap  H  dist-ℤ H (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
            (mul-int-ℕ ((q *ℕ s) +ℕ 1) (succ-ℕ x))
         dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)))
          ((int-ℕ (q *ℕ t)) *ℤ (int-ℕ y))
          by ap  H  dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)))
            (H *ℤ (int-ℕ y)))
            (mul-int-ℕ q t)
         dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)))
          (int-ℕ ((q *ℕ t) *ℕ y))
          by ap (dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x))))
            (mul-int-ℕ (q *ℕ t) y)
         dist-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x))
          ((q *ℕ t) *ℕ y)
          by dist-int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x))
            ((q *ℕ t) *ℕ y)

  sx-ty-case-split (inr tysx) =
    (abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) ,
      (q *ℕ t) , inv (dist-eqn))
    where
    rewrite-dist : (t *ℕ y) +ℕ d  (s *ℕ (succ-ℕ x))
    rewrite-dist =
      rewrite-right-dist-add-ℕ
        ( t *ℕ y)
        ( d)
        ( s *ℕ (succ-ℕ x))
        ( tysx)
        ( inv (dist-sx-ty-eq-d) 
          symmetric-dist-ℕ (s *ℕ (succ-ℕ x)) (t *ℕ y))

    quotient-min-dist-succ-x-nonzero : is-nonzero-ℕ q
    quotient-min-dist-succ-x-nonzero iszero =
      contradiction-le-ℕ (succ-ℕ x) d le-x-d leq-d-x
      where
      x-r-equality : succ-ℕ x  r
      x-r-equality =
        equational-reasoning
          succ-ℕ x
           (q *ℕ d) +ℕ r
            by (inv (eq-euclidean-division-ℕ d (succ-ℕ x)))
           (0 *ℕ d) +ℕ r
            by (ap  H  (H *ℕ d) +ℕ r) iszero)
           0 +ℕ r
            by (ap (_+ℕ r) (left-zero-law-mul-ℕ d))
           r
            by (left-unit-law-add-ℕ r)

      le-x-d : le-ℕ (succ-ℕ x) d
      le-x-d =
        tr
          ( λ n  le-ℕ n d)
          ( inv (x-r-equality))
          ( remainder-min-dist-succ-x-le-min-dist x y)

      x-pos-dist : pos-distance-between-multiples (succ-ℕ x) y (succ-ℕ x)
      x-pos-dist H =
        pair'
          ( is-nonzero-succ-ℕ x)
          ( pair 1 (pair 0 (ap succ-ℕ (left-unit-law-add-ℕ x))))

      leq-d-x : leq-ℕ d (succ-ℕ x)
      leq-d-x =
        minimal-positive-distance-is-minimal (succ-ℕ x) y (succ-ℕ x) x-pos-dist

    min-dist-succ-x-coeff-nonzero : is-nonzero-ℕ s
    min-dist-succ-x-coeff-nonzero iszero =
      minimal-positive-distance-nonzero
        ( succ-ℕ x)
        ( y)
        ( tr
          ( is-nonzero-ℕ)
          ( inv (left-successor-law-add-ℕ x y))
          ( is-nonzero-succ-ℕ (x +ℕ y)))
        ( d-is-zero)
      where
      zero-addition : (t *ℕ y) +ℕ d  0
      zero-addition =
        equational-reasoning
          (t *ℕ y) +ℕ d
           (s *ℕ (succ-ℕ x))
            by rewrite-dist
           (zero-ℕ *ℕ (succ-ℕ x))
            by (ap (_*ℕ (succ-ℕ x)) iszero)
           zero-ℕ
            by (left-zero-law-mul-ℕ (succ-ℕ x))

      d-is-zero : is-zero-ℕ d
      d-is-zero = is-zero-right-is-zero-add-ℕ (t *ℕ y) d (zero-addition)

    coeff-nonnegative : leq-ℤ one-ℤ ((int-ℕ q) *ℤ (int-ℕ s))
    coeff-nonnegative = tr (leq-ℤ one-ℤ)
      (inv (mul-int-ℕ q s)) (leq-int-ℕ 1 (q *ℕ s)
        (leq-succ-le-ℕ 0 (q *ℕ s) (le-is-nonzero-ℕ (q *ℕ s)
          (is-nonzero-mul-ℕ q s quotient-min-dist-succ-x-nonzero
            min-dist-succ-x-coeff-nonzero))))

    add-dist-eqn :
      int-ℕ d 
      ((neg-ℤ (