Divisibility of integers

module elementary-number-theory.divisibility-integers where
Imports
open import elementary-number-theory.absolute-value-integers
open import elementary-number-theory.addition-integers
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.equality-integers
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.natural-numbers

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.functions
open import foundation.identity-types
open import foundation.negation
open import foundation.propositional-maps
open import foundation.propositions
open import foundation.unit-type
open import foundation.universe-levels

Idea

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

  div-ℤ m n := Σ (k : ℤ), k *ℤ m = n.

If n is a nonzero integer, then div-ℤ m n is always a proposition in the sense that the type div-ℤ m n contains at most one element.

We also introduce unit integers, which are integers that divide the integer 1, and an equivalence relation sim-unit-ℤ on the integers in which two integers x and y are equivalent if there exists a unit integer u such that ux = y. These two concepts help establish further properties of the divisibility relation on the integers.

Definitions

div-ℤ :     UU lzero
div-ℤ d x = Σ   k  k *ℤ d  x)

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

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

Unit integers

is-unit-ℤ :   UU lzero
is-unit-ℤ x = div-ℤ x one-ℤ

unit-ℤ : UU lzero
unit-ℤ = Σ  is-unit-ℤ

int-unit-ℤ : unit-ℤ  
int-unit-ℤ = pr1

is-unit-int-unit-ℤ : (x : unit-ℤ)  is-unit-ℤ (int-unit-ℤ x)
is-unit-int-unit-ℤ = pr2

div-is-unit-ℤ :
  (x y : )  is-unit-ℤ x  div-ℤ x y
pr1 (div-is-unit-ℤ x y (pair d p)) = y *ℤ d
pr2 (div-is-unit-ℤ x y (pair d p)) =
  associative-mul-ℤ y d x  (ap (y *ℤ_) p  right-unit-law-mul-ℤ y)

The equivalence relation sim-unit-ℤ

We define the equivalence relation sim-unit-ℤ in such a way that sim-unit-ℤ x y is always a proposition.

presim-unit-ℤ :     UU lzero
presim-unit-ℤ x y = Σ unit-ℤ  u  (pr1 u) *ℤ x  y)

sim-unit-ℤ :     UU lzero
sim-unit-ℤ x y = ¬ (is-zero-ℤ x × is-zero-ℤ y)  presim-unit-ℤ x y

Properties

Divisibility by a nonzero integer is a property

is-prop-div-ℤ : (d x : )  is-nonzero-ℤ d  is-prop (div-ℤ d x)
is-prop-div-ℤ d x f = is-prop-map-is-emb (is-emb-right-mul-ℤ d f) x

The divisibility relation is a preorder

Note that the divisibility relation on the integers is not antisymmetric.

refl-div-ℤ : (x : )  div-ℤ x x
pr1 (refl-div-ℤ x) = one-ℤ
pr2 (refl-div-ℤ x) = left-unit-law-mul-ℤ x

trans-div-ℤ :
  (x y z : )  div-ℤ x y  div-ℤ y z  div-ℤ x z
pr1 (trans-div-ℤ x y z (pair d p) (pair e q)) = e *ℤ d
pr2 (trans-div-ℤ x y z (pair d p) (pair e q)) =
  ( associative-mul-ℤ e d x) 
    ( ( ap (e *ℤ_) p) 
      ( q))

Every integer is divisible by 1

div-one-ℤ : (x : )  div-ℤ one-ℤ x
pr1 (div-one-ℤ x) = x
pr2 (div-one-ℤ x) = right-unit-law-mul-ℤ x

Every integer divides 0

div-zero-ℤ : (x : )  div-ℤ x zero-ℤ
pr1 (div-zero-ℤ x) = zero-ℤ
pr2 (div-zero-ℤ x) = left-zero-law-mul-ℤ x

Every integer that is divisible by 0 is 0

is-zero-div-zero-ℤ :
  (x : )  div-ℤ zero-ℤ x  is-zero-ℤ x
is-zero-div-zero-ℤ x (pair d p) = inv p  right-zero-law-mul-ℤ d

The quotient of x by one is x

eq-quotient-div-is-one-ℤ :
 (k x : )  is-one-ℤ k  (H : div-ℤ k x)  quotient-div-ℤ k x H  x
eq-quotient-div-is-one-ℤ .one-ℤ x refl H =
  ap
    ( quotient-div-ℤ one-ℤ x)
    ( inv
      ( eq-is-prop'
        ( is-prop-div-ℤ one-ℤ x  ()))
        ( div-one-ℤ x)
        ( H)))

If k divides x and k is 0 then x is 0

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

If x divides both y and z, then it divides y + z

div-add-ℤ : (x y z : )  div-ℤ x y  div-ℤ x z  div-ℤ x (y +ℤ z)
pr1 (div-add-ℤ x y z (pair d p) (pair e q)) = d +ℤ e
pr2 (div-add-ℤ x y z (pair d p) (pair e q)) =
  ( right-distributive-mul-add-ℤ d e x) 
  ( ap-add-ℤ p q)

If x divides y then x divides any multiple of y

div-mul-ℤ :
  (k x y : )  div-ℤ x y  div-ℤ x (k *ℤ y)
div-mul-ℤ k x y H =
  trans-div-ℤ x y (k *ℤ y) H (pair k refl)

If x divides y then it divides -y

div-neg-ℤ : (x y : )  div-ℤ x y  div-ℤ x (neg-ℤ y)
pr1 (div-neg-ℤ x y (pair d p)) = neg-ℤ d
pr2 (div-neg-ℤ x y (pair d p)) = left-negative-law-mul-ℤ d x  ap neg-ℤ p

If x divides y then -x divides y

neg-div-ℤ : (x y : )  div-ℤ x y  div-ℤ (neg-ℤ x) y
pr1 (neg-div-ℤ x y (pair d p)) = neg-ℤ d
pr2 (neg-div-ℤ x y (pair d p)) =
  equational-reasoning
    (neg-ℤ d) *ℤ (neg-ℤ x)
     neg-ℤ (d *ℤ (neg-ℤ x))
      by left-negative-law-mul-ℤ d (neg-ℤ x)
     neg-ℤ (neg-ℤ (d *ℤ x))
      by ap neg-ℤ (right-negative-law-mul-ℤ d x)
     (d *ℤ x)
      by neg-neg-ℤ (d *ℤ x)
     y
      by p

Multiplication preserves divisibility

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

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.

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)

Comparison of divisibility on and on

div-int-div-ℕ :
  {x y : }  div-ℕ x y  div-ℤ (int-ℕ x) (int-ℕ y)
pr1 (div-int-div-ℕ {x} {y} (pair d p)) = int-ℕ d
pr2 (div-int-div-ℕ {x} {y} (pair d p)) = mul-int-ℕ d x  ap int-ℕ p

div-div-int-ℕ :
  {x y : }  div-ℤ (int-ℕ x) (int-ℕ y)  div-ℕ x y
div-div-int-ℕ {zero-ℕ} {y} (pair d p) =
  div-eq-ℕ zero-ℕ y
    ( inv (is-injective-int-ℕ (is-zero-div-zero-ℤ (int-ℕ y) (pair d p))))
pr1 (div-div-int-ℕ {succ-ℕ x} {y} (pair d p)) = abs-ℤ d
pr2 (div-div-int-ℕ {succ-ℕ x} {y} (pair d p)) =
  is-injective-int-ℕ
    ( ( inv (mul-int-ℕ (abs-ℤ d) (succ-ℕ x))) 
      ( ( ap
          ( _*ℤ (inr (inr x)))
          { int-abs-ℤ d}
          { d}
          ( int-abs-is-nonnegative-ℤ d
            ( is-nonnegative-left-factor-mul-ℤ
              { d}
              { inr (inr x)}
              ( is-nonnegative-eq-ℤ (inv p) (is-nonnegative-int-ℕ y))
              ( star)))) 
        ( p)))

An integer is a unit if and only if it is 1 or -1.

is-one-or-neg-one-ℤ :   UU lzero
is-one-or-neg-one-ℤ x = (is-one-ℤ x) + (is-neg-one-ℤ x)

is-unit-one-ℤ : is-unit-ℤ one-ℤ
is-unit-one-ℤ = refl-div-ℤ one-ℤ

one-unit-ℤ : unit-ℤ
pr1 one-unit-ℤ = one-ℤ
pr2 one-unit-ℤ = is-unit-one-ℤ

is-unit-is-one-ℤ :
  (x : )  is-one-ℤ x  is-unit-ℤ x
is-unit-is-one-ℤ .one-ℤ refl = is-unit-one-ℤ

is-unit-neg-one-ℤ : is-unit-ℤ neg-one-ℤ
pr1 is-unit-neg-one-ℤ = neg-one-ℤ
pr2 is-unit-neg-one-ℤ = refl

neg-one-unit-ℤ : unit-ℤ
pr1 neg-one-unit-ℤ = neg-one-ℤ
pr2 neg-one-unit-ℤ = is-unit-neg-one-ℤ

is-unit-is-neg-one-ℤ :
  (x : )  is-neg-one-ℤ x  is-unit-ℤ x
is-unit-is-neg-one-ℤ .neg-one-ℤ refl = is-unit-neg-one-ℤ

is-unit-is-one-or-neg-one-ℤ :
  (x : )  is-one-or-neg-one-ℤ x  is-unit-ℤ x
is-unit-is-one-or-neg-one-ℤ x (inl p) = is-unit-is-one-ℤ x p
is-unit-is-one-or-neg-one-ℤ x (inr p) = is-unit-is-neg-one-ℤ x p

is-one-or-neg-one-is-unit-ℤ :
  (x : )  is-unit-ℤ x  is-one-or-neg-one-ℤ x
is-one-or-neg-one-is-unit-ℤ (inl zero-ℕ) (pair d p) = inr refl
is-one-or-neg-one-is-unit-ℤ (inl (succ-ℕ x)) (pair (inl zero-ℕ) p) =
  ex-falso (Eq-eq-ℤ (inv p  compute-mul-ℤ neg-one-ℤ (inl (succ-ℕ x))))
is-one-or-neg-one-is-unit-ℤ (inl (succ-ℕ x)) (pair (inl (succ-ℕ d)) p) =
  ex-falso (Eq-eq-ℤ (inv p  compute-mul-ℤ (inl (succ-ℕ d)) (inl (succ-ℕ x))))
is-one-or-neg-one-is-unit-ℤ (inl (succ-ℕ x)) (pair (inr (inl star)) p) =
  ex-falso (Eq-eq-ℤ (inv p  compute-mul-ℤ zero-ℤ (inl (succ-ℕ x))))
is-one-or-neg-one-is-unit-ℤ (inl (succ-ℕ x)) (pair (inr (inr zero-ℕ)) p) =
  ex-falso (Eq-eq-ℤ (inv p  compute-mul-ℤ one-ℤ (inl (succ-ℕ x))))
is-one-or-neg-one-is-unit-ℤ (inl (succ-ℕ x)) (pair (inr (inr (succ-ℕ d))) p) =
  ex-falso
    ( Eq-eq-ℤ (inv p  compute-mul-ℤ (inr (inr (succ-ℕ d))) (inl (succ-ℕ x))))
is-one-or-neg-one-is-unit-ℤ (inr (inl star)) (pair d p) =
  ex-falso (Eq-eq-ℤ (inv (right-zero-law-mul-ℤ d)  p))
is-one-or-neg-one-is-unit-ℤ (inr (inr zero-ℕ)) (pair d p) = inl refl
is-one-or-neg-one-is-unit-ℤ (inr (inr (succ-ℕ x))) (pair (inl zero-ℕ) p) =
  ex-falso (Eq-eq-ℤ (inv p  compute-mul-ℤ neg-one-ℤ (inr (inr (succ-ℕ x)))))
is-one-or-neg-one-is-unit-ℤ (inr (inr (succ-ℕ x))) (pair (inl (succ-ℕ d)) p) =
  ex-falso
    ( Eq-eq-ℤ (inv p  compute-mul-ℤ (inl (succ-ℕ d)) (inr (inr (succ-ℕ x)))))
is-one-or-neg-one-is-unit-ℤ (inr (inr (succ-ℕ x))) (pair (inr (inl star)) p) =
  ex-falso (Eq-eq-ℤ (inv p  compute-mul-ℤ zero-ℤ (inr (inr (succ-ℕ x)))))
is-one-or-neg-one-is-unit-ℤ (inr (inr (succ-ℕ x))) (pair (inr (inr zero-ℕ)) p) =
  ex-falso (Eq-eq-ℤ (inv p  compute-mul-ℤ one-ℤ (inr (inr (succ-ℕ x)))))
is-one-or-neg-one-is-unit-ℤ
  (inr (inr (succ-ℕ x))) (pair (inr (inr (succ-ℕ d))) p) =
  ex-falso
    ( Eq-eq-ℤ
      ( inv p  compute-mul-ℤ (inr (inr (succ-ℕ d))) (inr (inr (succ-ℕ x)))))

Units are idempotent

idempotent-is-unit-ℤ : {x : }  is-unit-ℤ x  x *ℤ x  one-ℤ
idempotent-is-unit-ℤ {x} H =
  f (is-one-or-neg-one-is-unit-ℤ x H)
  where
  f : is-one-or-neg-one-ℤ x  x *ℤ x  one-ℤ
  f (inl refl) = refl
  f (inr refl) = refl

abstract
  is-one-is-unit-int-ℕ : (x : )  is-unit-ℤ (int-ℕ x)  is-one-ℕ x
  is-one-is-unit-int-ℕ x H with is-one-or-neg-one-is-unit-ℤ (int-ℕ x) H
  ... | inl p = is-injective-int-ℕ p
  ... | inr p = ex-falso (tr is-nonnegative-ℤ p (is-nonnegative-int-ℕ x))

The product xy is a unit if and only if both x and y are units

is-unit-mul-ℤ :
  (x y : )  is-unit-ℤ x  is-unit-ℤ y  is-unit-ℤ (x *ℤ y)
pr1 (is-unit-mul-ℤ x y (pair d p) (pair e q)) = e *ℤ d
pr2 (is-unit-mul-ℤ x y (pair d p) (pair e q)) =
  ( associative-mul-ℤ e d (x *ℤ y)) 
    ( ( ap
        ( e *ℤ_)
        ( ( inv (associative-mul-ℤ d x y)) 
          ( ap (_*ℤ y) p))) 
      ( q))

mul-unit-ℤ : unit-ℤ  unit-ℤ  unit-ℤ
pr1 (mul-unit-ℤ (pair x H) (pair y K)) = x *ℤ y
pr2 (mul-unit-ℤ (pair x H) (pair y K)) = is-unit-mul-ℤ x y H K

is-unit-left-factor-mul-ℤ :
  (x y : )  is-unit-ℤ (x *ℤ y)  is-unit-ℤ x
pr1 (is-unit-left-factor-mul-ℤ x y (pair d p)) = d *ℤ y
pr2 (is-unit-left-factor-mul-ℤ x y (pair d p)) =
  associative-mul-ℤ d y x  (ap (d *ℤ_) (commutative-mul-ℤ y x)  p)

is-unit-right-factor-ℤ :
  (x y : )  is-unit-ℤ (x *ℤ y)  is-unit-ℤ y
is-unit-right-factor-ℤ x y (pair d p) =
  is-unit-left-factor-mul-ℤ y x
    ( pair d (ap (d *ℤ_) (commutative-mul-ℤ y x)  p))

The relations presim-unit-ℤ and sim-unit-ℤ are logically equivalent

sim-unit-presim-unit-ℤ :
  {x y : }  presim-unit-ℤ x y  sim-unit-ℤ x y
sim-unit-presim-unit-ℤ {x} {y} H f = H

presim-unit-sim-unit-ℤ :
  {x y : }  sim-unit-ℤ x y  presim-unit-ℤ x y
presim-unit-sim-unit-ℤ {inl x} {inl y} H = H  t  Eq-eq-ℤ (pr1 t))
presim-unit-sim-unit-ℤ {inl x} {inr y} H = H  t  Eq-eq-ℤ (pr1 t))
presim-unit-sim-unit-ℤ {inr x} {inl y} H = H  t  Eq-eq-ℤ (pr2 t))
pr1 (presim-unit-sim-unit-ℤ {inr (inl star)} {inr (inl star)} H) = one-unit-ℤ
pr2 (presim-unit-sim-unit-ℤ {inr (inl star)} {inr (inl star)} H) = refl
presim-unit-sim-unit-ℤ {inr (inl star)} {inr (inr y)} H =
  H  t  Eq-eq-ℤ (pr2 t))
presim-unit-sim-unit-ℤ {inr (inr x)} {inr (inl star)} H =
  H  t  Eq-eq-ℤ (pr1 t))
presim-unit-sim-unit-ℤ {inr (inr x)} {inr (inr y)} H =
  H  t  Eq-eq-ℤ (pr1 t))

The relations presim-unit-ℤ and sim-unit-ℤ relate zero-ℤ only to itself

is-nonzero-presim-unit-ℤ :
  {x y : }  presim-unit-ℤ x y  is-nonzero-ℤ x  is-nonzero-ℤ y
is-nonzero-presim-unit-ℤ {x} {y} (pair (pair v (pair u α)) β) f p =
  Eq-eq-ℤ (ap (_*ℤ u) (inv q)  (commutative-mul-ℤ v u  α))
  where
  q : is-zero-ℤ v
  q = is-injective-right-mul-ℤ x f {v} {zero-ℤ} (β  p)

is-nonzero-sim-unit-ℤ :
  {x y : }  sim-unit-ℤ x y  is-nonzero-ℤ x  is-nonzero-ℤ y
is-nonzero-sim-unit-ℤ H f =
  is-nonzero-presim-unit-ℤ (H (f  pr1)) f

is-zero-sim-unit-ℤ :
  {x y : }  sim-unit-ℤ x y  is-zero-ℤ x  is-zero-ℤ y
is-zero-sim-unit-ℤ {x} {y} H p =
  double-negation-elim-is-decidable
    ( has-decidable-equality-ℤ y zero-ℤ)
    ( λ g  g (inv (β g)  (ap ((u g) *ℤ_) p  right-zero-law-mul-ℤ (u g))))
  where
  K : is-nonzero-ℤ y  presim-unit-ℤ x y
  K g = H  {(pair u v)  g v})
  u : is-nonzero-ℤ y  
  u g = pr1 (pr1 (K g))
  v : is-nonzero-ℤ y  
  v g = pr1 (pr2 (pr1 (K g)))
  β : (g : is-nonzero-ℤ y)  (u g) *ℤ x  y
  β g = pr2 (K g)

The relations presim-unit-ℤ and sim-unit-ℤ are equivalence relations

refl-presim-unit-ℤ : (x : )  presim-unit-ℤ x x
pr1 (refl-presim-unit-ℤ x) = one-unit-ℤ
pr2 (refl-presim-unit-ℤ x) = left-unit-law-mul-ℤ x

refl-sim-unit-ℤ : (x : )  sim-unit-ℤ x x
refl-sim-unit-ℤ x f = refl-presim-unit-ℤ x

presim-unit-eq-ℤ : {x y : }  x  y  presim-unit-ℤ x y
presim-unit-eq-ℤ {x} refl = refl-presim-unit-ℤ x

sim-unit-eq-ℤ : {x y : }  x  y  sim-unit-ℤ x y
sim-unit-eq-ℤ {x} refl = refl-sim-unit-ℤ x

symm-presim-unit-ℤ : {x y : }  presim-unit-ℤ x y  presim-unit-ℤ y x
symm-presim-unit-ℤ {x} {y} (pair (pair u H) p) =
  f (is-one-or-neg-one-is-unit-ℤ u H)
  where
  f : is-one-or-neg-one-ℤ u  presim-unit-ℤ y x
  pr1 (f (inl refl)) = one-unit-ℤ
  pr2 (f (inl refl)) = inv p
  pr1 (f (inr refl)) = neg-one-unit-ℤ
  pr2 (f (inr refl)) = inv (inv (neg-neg-ℤ x)  ap (neg-one-ℤ *ℤ_) p)

symm-sim-unit-ℤ : {x y : }  sim-unit-ℤ x y  sim-unit-ℤ y x
symm-sim-unit-ℤ {x} {y} H f =
  symm-presim-unit-ℤ (H  p  f (pair (pr2 p) (pr1 p))))

is-nonzero-sim-unit-ℤ' :
  {x y : }  sim-unit-ℤ x y  is-nonzero-ℤ y  is-nonzero-ℤ x
is-nonzero-sim-unit-ℤ' H = is-nonzero-sim-unit-ℤ (symm-sim-unit-ℤ H)

is-zero-sim-unit-ℤ' :
  {x y : }  sim-unit-ℤ x y  is-zero-ℤ y  is-zero-ℤ x
is-zero-sim-unit-ℤ' H = is-zero-sim-unit-ℤ (symm-sim-unit-ℤ H)

trans-presim-unit-ℤ :
  (x y z : )  presim-unit-ℤ x y  presim-unit-ℤ y z  presim-unit-ℤ x z
trans-presim-unit-ℤ x y z (pair (pair u H) p) (pair (pair v K) q) =
  f (is-one-or-neg-one-is-unit-ℤ u H) (is-one-or-neg-one-is-unit-ℤ v K)
  where
  f : is-one-or-neg-one-ℤ u  is-one-or-neg-one-ℤ v  presim-unit-ℤ x z
  pr1 (f (inl refl) (inl refl)) = one-unit-ℤ
  pr2 (f (inl refl) (inl refl)) = p  q
  pr1 (f (inl refl) (inr refl)) = neg-one-unit-ℤ
  pr2 (f (inl refl) (inr refl)) = ap neg-ℤ p  q
  pr1 (f (inr refl) (inl refl)) = neg-one-unit-ℤ
  pr2 (f (inr refl) (inl refl)) = p  q
  pr1 (f (inr refl) (inr refl)) = one-unit-ℤ
  pr2 (f (inr refl) (inr refl)) = inv (neg-neg-ℤ x)  (ap neg-ℤ p  q)

trans-sim-unit-ℤ :
  (x y z : )  sim-unit-ℤ x y  sim-unit-ℤ y z  sim-unit-ℤ x z
trans-sim-unit-ℤ x y z H K f =
  trans-presim-unit-ℤ x y z
    ( H  {(pair p q)  f (pair p (is-zero-sim-unit-ℤ K q))}))
    ( K  {(pair p q)  f (pair (is-zero-sim-unit-ℤ' H p) q)}))

sim-unit-ℤ x y holds if and only if x|y and y|x

antisymmetric-div-ℤ :
  (x y : )  div-ℤ x y  div-ℤ y x  sim-unit-ℤ x y
antisymmetric-div-ℤ x y (pair d p) (pair e q) H =
  f (is-decidable-is-zero-ℤ x)
  where
  f : is-decidable (is-zero-ℤ x)  presim-unit-ℤ x y
  f (inl refl) = presim-unit-eq-ℤ (inv (right-zero-law-mul-ℤ d)  p)
  pr1 (pr1 (f (inr g))) = d
  pr1 (pr2 (pr1 (f (inr g)))) = e
  pr2 (pr2 (pr1 (f (inr g)))) =
    is-injective-left-mul-ℤ x g
      ( ( commutative-mul-ℤ x (e *ℤ d)) 
        ( ( associative-mul-ℤ e d x) 
          ( ( ap (e *ℤ_) p) 
            ( q  inv (right-unit-law-mul-ℤ x)))))
  pr2 (f (inr g)) = p

sim-unit-ℤ |x| x holds

sim-unit-abs-ℤ : (x : )  sim-unit-ℤ (int-abs-ℤ x) x
pr1 (sim-unit-abs-ℤ (inl x) f) = neg-one-unit-ℤ
pr2 (sim-unit-abs-ℤ (inl x) f) = refl
sim-unit-abs-ℤ (inr (inl star)) = refl-sim-unit-ℤ zero-ℤ
sim-unit-abs-ℤ (inr (inr x)) = refl-sim-unit-ℤ (inr (inr x))

div-presim-unit-ℤ :
  {x y x' y' : }  presim-unit-ℤ x x'  presim-unit-ℤ y y' 
  div-ℤ x y  div-ℤ x' y'
pr1 (div-presim-unit-ℤ {x} {y} {x'} {y'} (pair u q) (pair v r) (pair d p)) =
  ((int-unit-ℤ v) *ℤ d) *ℤ (int-unit-ℤ u)
pr2 (div-presim-unit-ℤ {x} {y} {x'} {y'} (pair u q) (pair v r) (pair d p)) =
  ( ap ((((int-unit-ℤ v) *ℤ d) *ℤ (int-unit-ℤ u)) *ℤ_) (inv q)) 
  ( ( associative-mul-ℤ
      ( (int-unit-ℤ v) *ℤ d)
      ( int-unit-ℤ u)
      ( (int-unit-ℤ u) *ℤ x)) 
    ( ( ap
        ( ((int-unit-ℤ v) *ℤ d) *ℤ_)
        ( ( inv (associative-mul-ℤ (int-unit-ℤ u) (int-unit-ℤ u) x)) 
          ( ap (_*ℤ x) (idempotent-is-unit-ℤ (is-unit-int-unit-ℤ u))))) 
      ( ( associative-mul-ℤ (int-unit-ℤ v) d x) 
        ( ( ap ((int-unit-ℤ v) *ℤ_) p) 
          ( r)))))

div-sim-unit-ℤ :
  {x y x' y' : }  sim-unit-ℤ x x'  sim-unit-ℤ y y' 
  div-ℤ x y  div-ℤ x' y'
div-sim-unit-ℤ {x} {y} {x'} {y'} H K =
  div-presim-unit-ℤ (presim-unit-sim-unit-ℤ H) (presim-unit-sim-unit-ℤ K)

div-int-abs-div-ℤ :
  {x y : }  div-ℤ x y  div-ℤ (int-abs-ℤ x) y
div-int-abs-div-ℤ {x} {y} =
  div-sim-unit-ℤ (symm-sim-unit-ℤ (sim-unit-abs-ℤ x)) (refl-sim-unit-ℤ y)

div-div-int-abs-ℤ :
  {x y : }  div-ℤ (int-abs-ℤ x) y  div-ℤ x y
div-div-int-abs-ℤ {x} {y} =
  div-sim-unit-ℤ (sim-unit-abs-ℤ x) (refl-sim-unit-ℤ y)

If we have that sim-unit-ℤ x y, then they must differ only by sign

is-plus-or-minus-sim-unit-ℤ :
  {x y : }  sim-unit-ℤ x y  is-plus-or-minus-ℤ x y
is-plus-or-minus-sim-unit-ℤ {x} {y} H with ( is-decidable-is-zero-ℤ x)
is-plus-or-minus-sim-unit-ℤ {x} {y} H | inl z =
  inl (z  inv (is-zero-sim-unit-ℤ H z))
is-plus-or-minus-sim-unit-ℤ {x} {y} H | inr nz
  with
  ( is-one-or-neg-one-is-unit-ℤ
    ( int-unit-ℤ (pr1 (H  u  nz (pr1 u)))))
    ( is-unit-int-unit-ℤ (pr1 (H  u  nz (pr1 u))))))
is-plus-or-minus-sim-unit-ℤ {x} {y} H | inr nz | inl pos =
  inl
    ( equational-reasoning
      x
       one-ℤ *ℤ x
        by (inv (left-unit-law-mul-ℤ x))
       (int-unit-ℤ (pr1 (H  u  nz (pr1 u))))) *ℤ x
        by inv (ap (_*ℤ x) pos)
       y
        by pr2 (H  u  nz (pr1 u))))
is-plus-or-minus-sim-unit-ℤ {x} {y} H | inr nz | inr p =
  inr
    ( equational-reasoning
      neg-ℤ x
       (int-unit-ℤ (pr1 (H  u  nz (pr1 u))))) *ℤ x
        by ap (_*ℤ x) (inv p)
       y
        by pr2 (H  u  nz (pr1 u))))

If sim-unit-ℤ x y holds and both x and y have the same sign, then x = y

eq-sim-unit-is-nonnegative-ℤ :
  {a b : }  is-nonnegative-ℤ a  is-nonnegative-ℤ b  sim-unit-ℤ a b  a  b
eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K
  with is-plus-or-minus-sim-unit-ℤ K
eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inl pos = pos
eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg
  with is-decidable-is-zero-ℤ a
eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg | inl z =
  equational-reasoning
    a
     zero-ℤ
      by z
     neg-ℤ a
      by inv (ap neg-ℤ z)
     b
      by neg
eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg | inr nz =
  ex-falso ( nz ( is-zero-is-nonnegative-neg-is-nonnegative-ℤ
   a H (tr is-nonnegative-ℤ (inv neg) H')))