# Addition on the natural numbers

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Raymond Baker and malarbol.

Created on 2022-01-26.

module elementary-number-theory.addition-natural-numbers where

Imports
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.interchange-law
open import foundation.negated-equality
open import foundation.sets


## Definition

add-ℕ : ℕ → ℕ → ℕ

infixl 35 _+ℕ_

{-# BUILTIN NATPLUS _+ℕ_ #-}

add-ℕ' : ℕ → ℕ → ℕ

{m n m' n' : ℕ} → m ＝ m' → n ＝ n' → m +ℕ n ＝ m' +ℕ n'


## Properties

### The left and right unit laws

right-unit-law-add-ℕ :
(x : ℕ) → x +ℕ zero-ℕ ＝ x

(x : ℕ) → zero-ℕ +ℕ x ＝ x


### The left and right successor laws

abstract
(x y : ℕ) → (succ-ℕ x) +ℕ y ＝ succ-ℕ (x +ℕ y)

(x y : ℕ) → x +ℕ (succ-ℕ y) ＝ succ-ℕ (x +ℕ y)


abstract
(x y z : ℕ) → (x +ℕ y) +ℕ z ＝ x +ℕ (y +ℕ z)
associative-add-ℕ x y zero-ℕ = refl
associative-add-ℕ x y (succ-ℕ z) = ap succ-ℕ (associative-add-ℕ x y z)


abstract
commutative-add-ℕ : (x y : ℕ) → x +ℕ y ＝ y +ℕ x


### Addition by 1 on the left or on the right is the successor

abstract
(x : ℕ) → 1 +ℕ x ＝ succ-ℕ x

(x : ℕ) → x +ℕ 1 ＝ succ-ℕ x


### Addition by 1 on the left or on the right is the double successor

abstract
(x : ℕ) → 2 +ℕ x ＝ succ-ℕ (succ-ℕ x)

(x : ℕ) → x +ℕ 2 ＝ succ-ℕ (succ-ℕ x)


abstract
interchange-law-commutative-and-associative


### Addition by a fixed element on either side is injective

abstract
is-injective-right-add-ℕ : (k : ℕ) → is-injective (_+ℕ k)

is-injective-left-add-ℕ : (k : ℕ) → is-injective (k +ℕ_)
is-injective-left-add-ℕ k {x} {y} p =
( k)


### Addition by a fixed element on either side is an embedding

abstract
is-emb-left-add-ℕ : (x : ℕ) → is-emb (x +ℕ_)

is-emb-right-add-ℕ : (x : ℕ) → is-emb (_+ℕ x)


### x + y ＝ 0 if and only if both x and y are 0

abstract
(x y : ℕ) → is-zero-ℕ (x +ℕ y) → is-zero-ℕ y
is-zero-right-is-zero-add-ℕ x zero-ℕ p = refl
is-zero-right-is-zero-add-ℕ x (succ-ℕ y) p =
ex-falso (is-nonzero-succ-ℕ (x +ℕ y) p)

(x y : ℕ) → is-zero-ℕ (x +ℕ y) → is-zero-ℕ x

is-zero-summand-is-zero-sum-ℕ :
(x y : ℕ) → is-zero-ℕ (x +ℕ y) → (is-zero-ℕ x) × (is-zero-ℕ y)
is-zero-summand-is-zero-sum-ℕ x y p =

is-zero-sum-is-zero-summand-ℕ :
(x y : ℕ) → (is-zero-ℕ x) × (is-zero-ℕ y) → is-zero-ℕ (x +ℕ y)
is-zero-sum-is-zero-summand-ℕ .zero-ℕ .zero-ℕ (pair refl refl) = refl


### m ≠ m + n + 1

abstract