The difference between integers

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

Created on 2022-01-26.
Last modified on 2024-04-09.

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


Two integers with a difference equal to zero are equal

  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)

The difference of an integer with itself is zero

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

The difference of two equal integers is zero

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

The difference of zero and an integer is its negative

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

The difference of an integer with zero is itself

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

Differences with the predecessor or successor of an integer

  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)

Triangular identity for addition and difference of integers

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

The negative of the difference of two integers x and y is the difference of y and x

  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 laws for addition and difference of integers

  interchange-law-add-diff-ℤ :
    (x y u v : )  (x -ℤ y) +ℤ (u -ℤ v)  (x +ℤ u) -ℤ (y +ℤ v)
  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-ℤ :
    (x y u v : )  (x +ℤ y) -ℤ (u +ℤ v)  (x -ℤ u) +ℤ (y -ℤ v)
  interchange-law-diff-add-ℤ x y u v = inv (interchange-law-add-diff-ℤ x u y v)

The difference of integers is invariant by translation

  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)

The difference of the successors of two integers is their difference

  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