The difference between integers

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

Created on 2022-01-26.
Last modified on 2023-09-10.

module elementary-number-theory.difference-integers where
open import elementary-number-theory.addition-integers
open import elementary-number-theory.integers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.identity-types
open import foundation.interchange-law


Since integers of the form x - y occur often, we introduce them here and derive their basic properties relative to succ-ℤ, neg-ℤ, and add-ℤ. The file multiplication-integers imports difference-integers and more properties are derived there.


diff-ℤ :     
diff-ℤ x y = x +ℤ (neg-ℤ y)

infixl 36 _-ℤ_
_-ℤ_ = diff-ℤ


ap-diff-ℤ : {x x' y y' : }  x  x'  y  y'  x -ℤ y  x' -ℤ y'
ap-diff-ℤ p q = ap-binary diff-ℤ p q

eq-diff-ℤ : {x y : }  is-zero-ℤ (x -ℤ y)  x  y
eq-diff-ℤ {x} {y} H =
  ( inv (right-unit-law-add-ℤ x)) 
  ( ( ap (x +ℤ_) (inv (left-inverse-law-add-ℤ y))) 
    ( ( inv (associative-add-ℤ x (neg-ℤ y) y)) 
      ( ( ap (_+ℤ y) H) 
        ( left-unit-law-add-ℤ y))))

is-zero-diff-ℤ' : (x : )  is-zero-ℤ (x -ℤ x)
is-zero-diff-ℤ' = right-inverse-law-add-ℤ

is-zero-diff-ℤ :
  {x y : }  x  y  is-zero-ℤ (x -ℤ y)
is-zero-diff-ℤ {x} {.x} refl = is-zero-diff-ℤ' x

left-zero-law-diff-ℤ : (x : )  zero-ℤ -ℤ x  neg-ℤ x
left-zero-law-diff-ℤ x = left-unit-law-add-ℤ (neg-ℤ x)

right-zero-law-diff-ℤ : (x : )  x -ℤ zero-ℤ  x
right-zero-law-diff-ℤ x = right-unit-law-add-ℤ x

left-successor-law-diff-ℤ :
  (x y : )  (succ-ℤ x) -ℤ y  succ-ℤ (x -ℤ y)
left-successor-law-diff-ℤ x y = left-successor-law-add-ℤ x (neg-ℤ y)

right-successor-law-diff-ℤ :
  (x y : )  x -ℤ (succ-ℤ y)  pred-ℤ (x -ℤ y)
right-successor-law-diff-ℤ x y =
  ap (x +ℤ_) (neg-succ-ℤ y)  right-predecessor-law-add-ℤ x (neg-ℤ y)

left-predecessor-law-diff-ℤ :
  (x y : )  (pred-ℤ x) -ℤ y  pred-ℤ (x -ℤ y)
left-predecessor-law-diff-ℤ x y = left-predecessor-law-add-ℤ x (neg-ℤ y)

right-predecessor-law-diff-ℤ :
  (x y : )  x -ℤ (pred-ℤ y)  succ-ℤ (x -ℤ y)
right-predecessor-law-diff-ℤ x y =
  ap (x +ℤ_) (neg-pred-ℤ y)  right-successor-law-add-ℤ x (neg-ℤ y)

triangle-diff-ℤ :
  (x y z : )  (x -ℤ y) +ℤ (y -ℤ z)  x -ℤ z
triangle-diff-ℤ x y z =
  ( associative-add-ℤ x (neg-ℤ y) (y -ℤ z)) 
  ( ap
    ( x +ℤ_)
    ( ( inv (associative-add-ℤ (neg-ℤ y) y (neg-ℤ z))) 
      ( ( ap (_+ℤ (neg-ℤ z)) (left-inverse-law-add-ℤ y)) 
        ( left-unit-law-add-ℤ (neg-ℤ z)))))

distributive-neg-diff-ℤ :
  (x y : )  neg-ℤ (x -ℤ y)  y -ℤ x
distributive-neg-diff-ℤ x y =
  ( distributive-neg-add-ℤ x (neg-ℤ y)) 
  ( ( ap ((neg-ℤ x) +ℤ_) (neg-neg-ℤ y)) 
    ( commutative-add-ℤ (neg-ℤ x) y))

interchange-law-add-diff-ℤ : interchange-law add-ℤ diff-ℤ
interchange-law-add-diff-ℤ x y u v =
  ( interchange-law-add-add-ℤ x (neg-ℤ y) u (neg-ℤ v)) 
  ( ap ((x +ℤ u) +ℤ_) (inv (distributive-neg-add-ℤ y v)))

interchange-law-diff-add-ℤ : interchange-law diff-ℤ add-ℤ
interchange-law-diff-add-ℤ x y u v = inv (interchange-law-add-diff-ℤ x u y v)

left-translation-diff-ℤ :
  (x y z : )  (z +ℤ x) -ℤ (z +ℤ y)  x -ℤ y
left-translation-diff-ℤ x y z =
  ( interchange-law-diff-add-ℤ z x z y) 
  ( ( ap (_+ℤ (x -ℤ y)) (right-inverse-law-add-ℤ z)) 
    ( left-unit-law-add-ℤ (x -ℤ y)))

right-translation-diff-ℤ :
  (x y z : )  (x +ℤ z) -ℤ (y +ℤ z)  x -ℤ y
right-translation-diff-ℤ x y z =
  ( ap-diff-ℤ (commutative-add-ℤ x z) (commutative-add-ℤ y z)) 
  ( left-translation-diff-ℤ x y z)
diff-succ-ℤ : (x y : )  (succ-ℤ x) -ℤ (succ-ℤ y)  x -ℤ y
diff-succ-ℤ x y =
  ( ap ((succ-ℤ x) +ℤ_) (neg-succ-ℤ y)) 
  ( ( left-successor-law-add-ℤ x (pred-ℤ (neg-ℤ y))) 
    ( ( ap succ-ℤ (right-predecessor-law-add-ℤ x (neg-ℤ y))) 
      ( is-section-pred-ℤ (x -ℤ y))))

Recent changes