# Addition on the integers

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

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

module elementary-number-theory.addition-integers where

Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.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.positive-integers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.binary-embeddings
open import foundation.binary-equivalences
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.interchange-law
open import foundation.sets
open import foundation.unit-type


## Idea

We introduce addition on the integers and derive its basic properties with respect to succ-ℤ and neg-ℤ.

## Definition

add-ℤ : ℤ → ℤ → ℤ
add-ℤ (inl zero-ℕ) l = pred-ℤ l
add-ℤ (inl (succ-ℕ x)) l = pred-ℤ (add-ℤ (inl x) l)
add-ℤ (inr (inl star)) l = l
add-ℤ (inr (inr zero-ℕ)) l = succ-ℤ l
add-ℤ (inr (inr (succ-ℕ x))) l = succ-ℤ (add-ℤ (inr (inr x)) l)

add-ℤ' : ℤ → ℤ → ℤ
add-ℤ' x y = add-ℤ y x

infixl 35 _+ℤ_
_+ℤ_ = add-ℤ

ap-add-ℤ :
{x y x' y' : ℤ} → x ＝ x' → y ＝ y' → x +ℤ y ＝ x' +ℤ y'
ap-add-ℤ p q = ap-binary add-ℤ p q


## Properties

### Unit laws

abstract
left-unit-law-add-ℤ : (k : ℤ) → zero-ℤ +ℤ k ＝ k
left-unit-law-add-ℤ k = refl

right-unit-law-add-ℤ : (k : ℤ) → k +ℤ zero-ℤ ＝ k
right-unit-law-add-ℤ (inl zero-ℕ) = refl
right-unit-law-add-ℤ (inl (succ-ℕ x)) =
ap pred-ℤ (right-unit-law-add-ℤ (inl x))
right-unit-law-add-ℤ (inr (inl star)) = refl
right-unit-law-add-ℤ (inr (inr zero-ℕ)) = refl
right-unit-law-add-ℤ (inr (inr (succ-ℕ x))) =
ap succ-ℤ (right-unit-law-add-ℤ (inr (inr x)))


### Left and right predecessor laws

abstract
left-predecessor-law-add-ℤ :
(x y : ℤ) → pred-ℤ x +ℤ y ＝ pred-ℤ (x +ℤ y)
left-predecessor-law-add-ℤ (inl n) y = refl
left-predecessor-law-add-ℤ (inr (inl star)) y = refl
left-predecessor-law-add-ℤ (inr (inr zero-ℕ)) y =
inv (is-retraction-pred-ℤ y)
left-predecessor-law-add-ℤ (inr (inr (succ-ℕ x))) y =
inv (is-retraction-pred-ℤ ((inr (inr x)) +ℤ y))

right-predecessor-law-add-ℤ :
(x y : ℤ) → x +ℤ pred-ℤ y ＝ pred-ℤ (x +ℤ y)
right-predecessor-law-add-ℤ (inl zero-ℕ) n = refl
right-predecessor-law-add-ℤ (inl (succ-ℕ m)) n =
ap pred-ℤ (right-predecessor-law-add-ℤ (inl m) n)
right-predecessor-law-add-ℤ (inr (inl star)) n = refl
right-predecessor-law-add-ℤ (inr (inr zero-ℕ)) n =
equational-reasoning
succ-ℤ (pred-ℤ n)
＝ n
by is-section-pred-ℤ n
＝ pred-ℤ (succ-ℤ n)
by inv (is-retraction-pred-ℤ n)
right-predecessor-law-add-ℤ (inr (inr (succ-ℕ x))) n =
equational-reasoning
succ-ℤ (inr (inr x) +ℤ pred-ℤ n)
＝ succ-ℤ (pred-ℤ (inr (inr x) +ℤ n))
by ap succ-ℤ (right-predecessor-law-add-ℤ (inr (inr x)) n)
＝ inr (inr x) +ℤ n
by is-section-pred-ℤ ((inr (inr x)) +ℤ n)
＝ pred-ℤ (succ-ℤ (inr (inr x) +ℤ n))
by inv (is-retraction-pred-ℤ ((inr (inr x)) +ℤ n))


### Left and right successor laws

abstract
left-successor-law-add-ℤ :
(x y : ℤ) → succ-ℤ x +ℤ y ＝ succ-ℤ (x +ℤ y)
left-successor-law-add-ℤ (inl zero-ℕ) y =
inv (is-section-pred-ℤ y)
left-successor-law-add-ℤ (inl (succ-ℕ x)) y =
equational-reasoning
inl x +ℤ y
＝ succ-ℤ (pred-ℤ (inl x +ℤ y))
by inv (is-section-pred-ℤ ((inl x) +ℤ y))
＝ succ-ℤ (pred-ℤ (inl x) +ℤ y)
by ap succ-ℤ (inv (left-predecessor-law-add-ℤ (inl x) y))
left-successor-law-add-ℤ (inr (inl star)) y = refl
left-successor-law-add-ℤ (inr (inr x)) y = refl

right-successor-law-add-ℤ :
(x y : ℤ) → x +ℤ succ-ℤ y ＝ succ-ℤ (x +ℤ y)
right-successor-law-add-ℤ (inl zero-ℕ) y =
equational-reasoning
pred-ℤ (succ-ℤ y)
＝ y
by is-retraction-pred-ℤ y
＝ succ-ℤ (pred-ℤ y)
by inv (is-section-pred-ℤ y)
right-successor-law-add-ℤ (inl (succ-ℕ x)) y =
equational-reasoning
pred-ℤ (inl x +ℤ succ-ℤ y)
＝ pred-ℤ (succ-ℤ (inl x +ℤ y))
by ap pred-ℤ (right-successor-law-add-ℤ (inl x) y)
＝ inl x +ℤ y
by is-retraction-pred-ℤ ((inl x) +ℤ y)
＝ succ-ℤ (pred-ℤ (inl x +ℤ y))
by inv (is-section-pred-ℤ ((inl x) +ℤ y))
right-successor-law-add-ℤ (inr (inl star)) y = refl
right-successor-law-add-ℤ (inr (inr zero-ℕ)) y = refl
right-successor-law-add-ℤ (inr (inr (succ-ℕ x))) y =
ap succ-ℤ (right-successor-law-add-ℤ (inr (inr x)) y)


### The successor of an integer is that integer plus one

abstract
is-right-add-one-succ-ℤ : (x : ℤ) → succ-ℤ x ＝ x +ℤ one-ℤ
is-right-add-one-succ-ℤ x =
equational-reasoning
succ-ℤ x
＝ succ-ℤ (x +ℤ zero-ℤ)
by inv (ap succ-ℤ (right-unit-law-add-ℤ x))
＝ x +ℤ one-ℤ
by inv (right-successor-law-add-ℤ x zero-ℤ)

is-left-add-one-succ-ℤ : (x : ℤ) → succ-ℤ x ＝ one-ℤ +ℤ x
is-left-add-one-succ-ℤ x = inv (left-successor-law-add-ℤ zero-ℤ x)

left-add-one-ℤ : (x : ℤ) → one-ℤ +ℤ x ＝ succ-ℤ x
left-add-one-ℤ x = refl

right-add-one-ℤ : (x : ℤ) → x +ℤ one-ℤ ＝ succ-ℤ x
right-add-one-ℤ x = inv (is-right-add-one-succ-ℤ x)


### The predecessor of an integer is that integer minus one

  is-left-add-neg-one-pred-ℤ : (x : ℤ) → pred-ℤ x ＝ neg-one-ℤ +ℤ x
is-left-add-neg-one-pred-ℤ x =
inv (left-predecessor-law-add-ℤ zero-ℤ x)

is-right-add-neg-one-pred-ℤ : (x : ℤ) → pred-ℤ x ＝ x +ℤ neg-one-ℤ
is-right-add-neg-one-pred-ℤ x =
equational-reasoning
pred-ℤ x
＝ pred-ℤ (x +ℤ zero-ℤ)
by inv (ap pred-ℤ (right-unit-law-add-ℤ x))
＝ x +ℤ neg-one-ℤ
by inv (right-predecessor-law-add-ℤ x zero-ℤ)

left-add-neg-one-ℤ : (x : ℤ) → neg-one-ℤ +ℤ x ＝ pred-ℤ x
left-add-neg-one-ℤ x = refl

right-add-neg-one-ℤ : (x : ℤ) → x +ℤ neg-one-ℤ ＝ pred-ℤ x
right-add-neg-one-ℤ x = inv (is-right-add-neg-one-pred-ℤ x)


### Addition is associative

abstract
associative-add-ℤ :
(x y z : ℤ) → ((x +ℤ y) +ℤ z) ＝ (x +ℤ (y +ℤ z))
associative-add-ℤ (inl zero-ℕ) y z =
equational-reasoning
(neg-one-ℤ +ℤ y) +ℤ z
＝ (pred-ℤ (zero-ℤ +ℤ y)) +ℤ z
by ap (_+ℤ z) (left-predecessor-law-add-ℤ zero-ℤ y)
＝ pred-ℤ (y +ℤ z)
by left-predecessor-law-add-ℤ y z
＝ neg-one-ℤ +ℤ (y +ℤ z)
by inv (left-predecessor-law-add-ℤ zero-ℤ (y +ℤ z))
associative-add-ℤ (inl (succ-ℕ x)) y z =
equational-reasoning
(pred-ℤ (inl x) +ℤ y) +ℤ z
＝ pred-ℤ (inl x +ℤ y) +ℤ z
by ap (_+ℤ z) (left-predecessor-law-add-ℤ (inl x) y)
＝ pred-ℤ ((inl x +ℤ y) +ℤ z)
by left-predecessor-law-add-ℤ ((inl x) +ℤ y) z
＝ pred-ℤ (inl x +ℤ (y +ℤ z))
by ap pred-ℤ (associative-add-ℤ (inl x) y z)
＝ pred-ℤ (inl x) +ℤ (y +ℤ z)
by inv (left-predecessor-law-add-ℤ (inl x) (y +ℤ z))
associative-add-ℤ (inr (inl star)) y z =
refl
associative-add-ℤ (inr (inr zero-ℕ)) y z =
equational-reasoning
(one-ℤ +ℤ y) +ℤ z
＝ succ-ℤ (zero-ℤ +ℤ y) +ℤ z
by ap (_+ℤ z) (left-successor-law-add-ℤ zero-ℤ y)
＝ succ-ℤ (y +ℤ z)
by left-successor-law-add-ℤ y z
＝ one-ℤ +ℤ (y +ℤ z)
by inv (left-successor-law-add-ℤ zero-ℤ (y +ℤ z))
associative-add-ℤ (inr (inr (succ-ℕ x))) y z =
equational-reasoning
(succ-ℤ (inr (inr x)) +ℤ y) +ℤ z
＝ succ-ℤ (inr (inr x) +ℤ y) +ℤ z
by ap (_+ℤ z) (left-successor-law-add-ℤ (inr (inr x)) y)
＝ succ-ℤ ((inr (inr x) +ℤ y) +ℤ z)
by left-successor-law-add-ℤ ((inr (inr x)) +ℤ y) z
＝ succ-ℤ (inr (inr x) +ℤ (y +ℤ z))
by ap succ-ℤ (associative-add-ℤ (inr (inr x)) y z)
＝ succ-ℤ (inr (inr x)) +ℤ (y +ℤ z)
by inv (left-successor-law-add-ℤ (inr (inr x)) (y +ℤ z))


### Addition is commutative

abstract
commutative-add-ℤ : (x y : ℤ) → x +ℤ y ＝ y +ℤ x
commutative-add-ℤ (inl zero-ℕ) y =
equational-reasoning
neg-one-ℤ +ℤ y
＝ pred-ℤ (zero-ℤ +ℤ y)
by left-predecessor-law-add-ℤ zero-ℤ y
＝ pred-ℤ (y +ℤ zero-ℤ)
by inv (ap pred-ℤ (right-unit-law-add-ℤ y))
＝ y +ℤ neg-one-ℤ
by inv (right-predecessor-law-add-ℤ y zero-ℤ)
commutative-add-ℤ (inl (succ-ℕ x)) y =
equational-reasoning
(inl (succ-ℕ x)) +ℤ y
＝ pred-ℤ (y +ℤ (inl x))
by ap pred-ℤ (commutative-add-ℤ (inl x) y)
＝ y +ℤ (inl (succ-ℕ x))
by inv (right-predecessor-law-add-ℤ y (inl x))
commutative-add-ℤ (inr (inl star)) y =
inv (right-unit-law-add-ℤ y)
commutative-add-ℤ (inr (inr zero-ℕ)) y =
equational-reasoning
succ-ℤ y
＝ succ-ℤ (y +ℤ zero-ℤ)
by inv (ap succ-ℤ (right-unit-law-add-ℤ y))
＝ y +ℤ one-ℤ
by inv (right-successor-law-add-ℤ y zero-ℤ)
commutative-add-ℤ (inr (inr (succ-ℕ x))) y =
equational-reasoning
succ-ℤ ((inr (inr x)) +ℤ y)
＝ succ-ℤ (y +ℤ (inr (inr x)))
by ap succ-ℤ (commutative-add-ℤ (inr (inr x)) y)
＝ y +ℤ (succ-ℤ (inr (inr x)))
by inv (right-successor-law-add-ℤ y (inr (inr x)))


### The inverse laws for addition and negatives

abstract
left-inverse-law-add-ℤ :
(x : ℤ) → neg-ℤ x +ℤ x ＝ zero-ℤ
left-inverse-law-add-ℤ (inl zero-ℕ) = refl
left-inverse-law-add-ℤ (inl (succ-ℕ x)) =
equational-reasoning
succ-ℤ (inr (inr x) +ℤ pred-ℤ (inl x))
＝ succ-ℤ (pred-ℤ (inr (inr x) +ℤ inl x))
by ap succ-ℤ (right-predecessor-law-add-ℤ (inr (inr x)) (inl x))
＝ inr (inr x) +ℤ inl x
by is-section-pred-ℤ ((inr (inr x)) +ℤ (inl x))
＝ zero-ℤ
by left-inverse-law-add-ℤ (inl x)
left-inverse-law-add-ℤ (inr (inl star)) = refl
left-inverse-law-add-ℤ (inr (inr x)) =
equational-reasoning
neg-ℤ (inr (inr x)) +ℤ inr (inr x)
＝ inr (inr x) +ℤ inl x
by commutative-add-ℤ (inl x) (inr (inr x))
＝ zero-ℤ
by left-inverse-law-add-ℤ (inl x)

right-inverse-law-add-ℤ :
(x : ℤ) → x +ℤ neg-ℤ x ＝ zero-ℤ
right-inverse-law-add-ℤ x =
equational-reasoning
x +ℤ neg-ℤ x
＝ neg-ℤ x +ℤ x
by commutative-add-ℤ x (neg-ℤ x)
＝ zero-ℤ
by left-inverse-law-add-ℤ x


### Interchange law for addition with respect to addition

abstract
interchange-law-add-add-ℤ :
(x y u v : ℤ) → (x +ℤ y) +ℤ (u +ℤ v) ＝ (x +ℤ u) +ℤ (y +ℤ v)
interchange-law-add-add-ℤ =
interchange-law-commutative-and-associative
add-ℤ
commutative-add-ℤ
associative-add-ℤ


### Addition by x is a binary equivalence

abstract
is-section-left-add-neg-ℤ :
(x y : ℤ) → x +ℤ (neg-ℤ x +ℤ y) ＝ y
is-section-left-add-neg-ℤ x y =
equational-reasoning
x +ℤ (neg-ℤ x +ℤ y)
＝ (x +ℤ neg-ℤ x) +ℤ y
by inv (associative-add-ℤ x (neg-ℤ x) y)
＝ y
by ap (_+ℤ y) (right-inverse-law-add-ℤ x)

is-retraction-left-add-neg-ℤ :
(x y : ℤ) → (neg-ℤ x) +ℤ (x +ℤ y) ＝ y
is-retraction-left-add-neg-ℤ x y =
equational-reasoning
neg-ℤ x +ℤ (x +ℤ y)
＝ (neg-ℤ x +ℤ x) +ℤ y
by inv (associative-add-ℤ (neg-ℤ x) x y)
＝ y
by ap (_+ℤ y) (left-inverse-law-add-ℤ x)

abstract
is-equiv-left-add-ℤ : (x : ℤ) → is-equiv (x +ℤ_)
pr1 (pr1 (is-equiv-left-add-ℤ x)) = add-ℤ (neg-ℤ x)
pr2 (pr1 (is-equiv-left-add-ℤ x)) = is-section-left-add-neg-ℤ x
pr1 (pr2 (is-equiv-left-add-ℤ x)) = add-ℤ (neg-ℤ x)
pr2 (pr2 (is-equiv-left-add-ℤ x)) = is-retraction-left-add-neg-ℤ x

equiv-left-add-ℤ : ℤ → (ℤ ≃ ℤ)
pr1 (equiv-left-add-ℤ x) = add-ℤ x
pr2 (equiv-left-add-ℤ x) = is-equiv-left-add-ℤ x

abstract
is-section-right-add-neg-ℤ :
(x y : ℤ) → (y +ℤ neg-ℤ x) +ℤ x ＝ y
is-section-right-add-neg-ℤ x y =
equational-reasoning
(y +ℤ neg-ℤ x) +ℤ x
＝ y +ℤ (neg-ℤ x +ℤ x)
by associative-add-ℤ y (neg-ℤ x) x
＝ y +ℤ zero-ℤ
by ap (y +ℤ_) (left-inverse-law-add-ℤ x)
＝ y
by right-unit-law-add-ℤ y

is-retraction-right-add-neg-ℤ :
(x y : ℤ) → (y +ℤ x) +ℤ neg-ℤ x ＝ y
is-retraction-right-add-neg-ℤ x y =
equational-reasoning
(y +ℤ x) +ℤ neg-ℤ x
＝ y +ℤ (x +ℤ neg-ℤ x)
by associative-add-ℤ y x (neg-ℤ x)
＝ y +ℤ zero-ℤ
by ap (y +ℤ_) (right-inverse-law-add-ℤ x)
＝ y
by right-unit-law-add-ℤ y

abstract
is-equiv-right-add-ℤ : (y : ℤ) → is-equiv (_+ℤ y)
pr1 (pr1 (is-equiv-right-add-ℤ y)) = _+ℤ (neg-ℤ y)
pr2 (pr1 (is-equiv-right-add-ℤ y)) = is-section-right-add-neg-ℤ y
pr1 (pr2 (is-equiv-right-add-ℤ y)) = _+ℤ (neg-ℤ y)
pr2 (pr2 (is-equiv-right-add-ℤ y)) = is-retraction-right-add-neg-ℤ y

equiv-right-add-ℤ : ℤ → (ℤ ≃ ℤ)
pr1 (equiv-right-add-ℤ y) = _+ℤ y
pr2 (equiv-right-add-ℤ y) = is-equiv-right-add-ℤ y

is-binary-equiv-left-add-ℤ : is-binary-equiv add-ℤ
pr1 is-binary-equiv-left-add-ℤ = is-equiv-right-add-ℤ
pr2 is-binary-equiv-left-add-ℤ = is-equiv-left-add-ℤ


### Addition by an integer is a binary embedding

abstract
is-emb-left-add-ℤ :
(x : ℤ) → is-emb (x +ℤ_)
is-emb-left-add-ℤ x =
is-emb-is-equiv (is-equiv-left-add-ℤ x)

is-emb-right-add-ℤ :
(y : ℤ) → is-emb (_+ℤ y)
is-emb-right-add-ℤ y = is-emb-is-equiv (is-equiv-right-add-ℤ y)

is-binary-emb-add-ℤ : is-binary-emb add-ℤ
is-binary-emb-add-ℤ =
is-binary-emb-is-binary-equiv is-binary-equiv-left-add-ℤ


### Addition by x is injective

abstract
is-injective-right-add-ℤ : (x : ℤ) → is-injective (_+ℤ x)
is-injective-right-add-ℤ x = is-injective-is-emb (is-emb-right-add-ℤ x)

is-injective-left-add-ℤ : (x : ℤ) → is-injective (x +ℤ_)
is-injective-left-add-ℤ x = is-injective-is-emb (is-emb-left-add-ℤ x)


### Negative laws for addition

abstract
right-negative-law-add-ℤ :
(k l : ℤ) → k +ℤ neg-ℤ l ＝ neg-ℤ (neg-ℤ k +ℤ l)
right-negative-law-add-ℤ (inl zero-ℕ) l =
equational-reasoning
neg-one-ℤ +ℤ neg-ℤ l
＝ pred-ℤ (zero-ℤ +ℤ neg-ℤ l)
by left-predecessor-law-add-ℤ zero-ℤ (neg-ℤ l)
＝ neg-ℤ (succ-ℤ l)
by pred-neg-ℤ l
right-negative-law-add-ℤ (inl (succ-ℕ x)) l =
equational-reasoning
pred-ℤ (inl x) +ℤ neg-ℤ l
＝ pred-ℤ (inl x +ℤ neg-ℤ l)
by left-predecessor-law-add-ℤ (inl x) (neg-ℤ l)
＝ pred-ℤ (neg-ℤ (neg-ℤ (inl x) +ℤ l))
by ap pred-ℤ (right-negative-law-add-ℤ (inl x) l)
＝ neg-ℤ (succ-ℤ (inr (inr x) +ℤ l))
by pred-neg-ℤ (inr (inr x) +ℤ l)
right-negative-law-add-ℤ (inr (inl star)) l =
refl
right-negative-law-add-ℤ (inr (inr zero-ℕ)) l =
inv (neg-pred-ℤ l)
right-negative-law-add-ℤ (inr (inr (succ-ℕ n))) l =
equational-reasoning
succ-ℤ (in-pos-ℤ n) +ℤ neg-ℤ l
＝ succ-ℤ (in-pos-ℤ n +ℤ neg-ℤ l)
by left-successor-law-add-ℤ (in-pos-ℤ n) (neg-ℤ l)
＝ succ-ℤ (neg-ℤ (neg-ℤ (inr (inr n)) +ℤ l))
by ap succ-ℤ (right-negative-law-add-ℤ (inr (inr n)) l)
＝ neg-ℤ (pred-ℤ ((inl n) +ℤ l))
by inv (neg-pred-ℤ ((inl n) +ℤ l))


### Distributivity of negatives over addition

abstract
distributive-neg-add-ℤ :
(k l : ℤ) → neg-ℤ (k +ℤ l) ＝ neg-ℤ k +ℤ neg-ℤ l
distributive-neg-add-ℤ (inl zero-ℕ) l =
equational-reasoning
neg-ℤ (inl zero-ℕ +ℤ l)
＝ neg-ℤ (pred-ℤ (zero-ℤ +ℤ l))
by ap neg-ℤ (left-predecessor-law-add-ℤ zero-ℤ l)
＝ neg-ℤ (inl zero-ℕ) +ℤ neg-ℤ l
by neg-pred-ℤ l
distributive-neg-add-ℤ (inl (succ-ℕ n)) l =
equational-reasoning
neg-ℤ (pred-ℤ (inl n +ℤ l))
＝ succ-ℤ (neg-ℤ (inl n +ℤ l))
by neg-pred-ℤ (inl n +ℤ l)
＝ succ-ℤ (neg-ℤ (inl n) +ℤ neg-ℤ l)
by ap succ-ℤ (distributive-neg-add-ℤ (inl n) l)
＝ neg-ℤ (pred-ℤ (inl n)) +ℤ neg-ℤ l
by ap (_+ℤ (neg-ℤ l)) (inv (neg-pred-ℤ (inl n)))
distributive-neg-add-ℤ (inr (inl star)) l =
refl
distributive-neg-add-ℤ (inr (inr zero-ℕ)) l =
inv (pred-neg-ℤ l)
distributive-neg-add-ℤ (inr (inr (succ-ℕ n))) l =
equational-reasoning
neg-ℤ (succ-ℤ (in-pos-ℤ n +ℤ l))
＝ pred-ℤ (neg-ℤ (in-pos-ℤ n +ℤ l))
by inv (pred-neg-ℤ (in-pos-ℤ n +ℤ l))
＝ pred-ℤ (neg-ℤ (inr (inr n)) +ℤ neg-ℤ l)
by ap pred-ℤ (distributive-neg-add-ℤ (inr (inr n)) l)


### The inclusion of ℕ into ℤ preserves addition

abstract
add-int-ℕ : (x y : ℕ) → (int-ℕ x) +ℤ (int-ℕ y) ＝ int-ℕ (x +ℕ y)
add-int-ℕ x zero-ℕ = right-unit-law-add-ℤ (int-ℕ x)
add-int-ℕ x (succ-ℕ y) =
equational-reasoning
int-ℕ x +ℤ int-ℕ (succ-ℕ y)
＝ int-ℕ x +ℤ succ-ℤ (int-ℕ y)
by ap ((int-ℕ x) +ℤ_) (inv (succ-int-ℕ y))
＝ succ-ℤ (int-ℕ x +ℤ int-ℕ y)
by right-successor-law-add-ℤ (int-ℕ x) (int-ℕ y)
＝ succ-ℤ (int-ℕ (x +ℕ y))
by ap succ-ℤ (add-int-ℕ x y)
＝ int-ℕ (succ-ℕ (x +ℕ y))
by succ-int-ℕ (x +ℕ y)


### If x + y = y then x = 0

abstract
is-zero-left-add-ℤ :
(x y : ℤ) → x +ℤ y ＝ y → is-zero-ℤ x
is-zero-left-add-ℤ x y H =
equational-reasoning
x
＝ x +ℤ zero-ℤ
by inv (right-unit-law-add-ℤ x)
＝ x +ℤ (y +ℤ neg-ℤ y)
by inv (ap (x +ℤ_) (right-inverse-law-add-ℤ y))
＝ (x +ℤ y) +ℤ neg-ℤ y
by inv (associative-add-ℤ x y (neg-ℤ y))
＝ y +ℤ neg-ℤ y
by ap (_+ℤ (neg-ℤ y)) H
＝ zero-ℤ
by right-inverse-law-add-ℤ y


### If x + y = x then y = 0

abstract
is-zero-right-add-ℤ :
(x y : ℤ) → x +ℤ y ＝ x → is-zero-ℤ y
is-zero-right-add-ℤ x y H =
is-zero-left-add-ℤ y x (commutative-add-ℤ y x ∙ H)