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