# Addition of positive, negative, nonnegative and nonpositive integers

Content created by Fredrik Bakke and malarbol.

Created on 2024-03-28.

module elementary-number-theory.addition-positive-and-negative-integers where

Imports
open import elementary-number-theory.addition-integers
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.negative-integers
open import elementary-number-theory.nonnegative-integers
open import elementary-number-theory.nonpositive-integers
open import elementary-number-theory.positive-and-negative-integers
open import elementary-number-theory.positive-integers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.unit-type


## Idea

When we have information about the sign of the summands, we can in many cases deduce the sign of their sum too. The table below tabulates all such cases and displays the corresponding Agda definition.

pqp +ℤ qoperation
positivepositivepositiveadd-positive-ℤ
positivenonnegativepositive
positivenegative
positivenonpositive
nonnegativepositivepositive
nonnegativenonnegativenonnegativeadd-nonnegative-ℤ
nonnegativenegative
nonnegativenonpositive
negativepositive
negativenonnegative
negativenegativenegativeadd-negative-ℤ
negativenonpositivenegative
nonpositivepositive
nonpositivenonnegative
nonpositivenegativenegative
nonpositivenonpositivenonpositiveadd-nonpositive-ℤ

## Lemmas

### The sum of two positive integers is positive

abstract
{x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y)
is-positive-add-ℤ {inr (inr zero-ℕ)} {y} H K =
is-positive-succ-is-positive-ℤ K
is-positive-add-ℤ {inr (inr (succ-ℕ x))} {y} H K =
is-positive-succ-is-positive-ℤ
( is-positive-add-ℤ {inr (inr x)} H K)


### The sum of a positive and a nonnegative integer is positive

abstract
{x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-positive-ℤ (x +ℤ y)
is-positive-add-positive-nonnegative-ℤ {inr (inr zero-ℕ)} {y} H K =
is-positive-succ-is-nonnegative-ℤ K
is-positive-add-positive-nonnegative-ℤ {inr (inr (succ-ℕ x))} {y} H K =
is-positive-succ-is-positive-ℤ
( is-positive-add-positive-nonnegative-ℤ {inr (inr x)} H K)


### The sum of a nonnegative and a positive integer is positive

abstract
{x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y)
is-positive-add-nonnegative-positive-ℤ {x} {y} H K =
is-positive-eq-ℤ
( commutative-add-ℤ y x)
( is-positive-add-positive-nonnegative-ℤ K H)


### The sum of two nonnegative integers is nonnegative

abstract
{x y : ℤ} →
is-nonnegative-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (x +ℤ y)
is-nonnegative-add-ℤ {inr (inl x)} {y} H K = K
is-nonnegative-add-ℤ {inr (inr zero-ℕ)} {y} H K =
is-nonnegative-succ-is-nonnegative-ℤ K
is-nonnegative-add-ℤ {inr (inr (succ-ℕ x))} {y} H K =
is-nonnegative-succ-is-nonnegative-ℤ
( is-nonnegative-add-ℤ {inr (inr x)} star K)


### The sum of two negative integers is negative

abstract
{x y : ℤ} → is-negative-ℤ x → is-negative-ℤ y → is-negative-ℤ (x +ℤ y)
is-negative-add-ℤ {x} {y} H K =
is-negative-eq-ℤ
( neg-neg-ℤ (x +ℤ y))
( is-negative-neg-is-positive-ℤ
( is-positive-eq-ℤ
( inv (distributive-neg-add-ℤ x y))
( is-positive-neg-is-negative-ℤ H)
( is-positive-neg-is-negative-ℤ K))))


### The sum of a negative and a nonpositive integer is negative

abstract
{x y : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ y → is-negative-ℤ (x +ℤ y)
is-negative-add-negative-nonnegative-ℤ {x} {y} H K =
is-negative-eq-ℤ
( neg-neg-ℤ (x +ℤ y))
( is-negative-neg-is-positive-ℤ
( is-positive-eq-ℤ
( inv (distributive-neg-add-ℤ x y))
( is-positive-neg-is-negative-ℤ H)
( is-nonnegative-neg-is-nonpositive-ℤ K))))


### The sum of a nonpositive and a negative integer is negative

abstract
{x y : ℤ} → is-nonpositive-ℤ x → is-negative-ℤ y → is-negative-ℤ (x +ℤ y)
is-negative-add-nonpositive-negative-ℤ {x} {y} H K =
is-negative-eq-ℤ
( commutative-add-ℤ y x)
( is-negative-add-negative-nonnegative-ℤ K H)


### The sum of two nonpositive integers is nonpositive

abstract
{x y : ℤ} →
is-nonpositive-ℤ x → is-nonpositive-ℤ y → is-nonpositive-ℤ (x +ℤ y)
is-nonpositive-add-ℤ {x} {y} H K =
is-nonpositive-eq-ℤ
( neg-neg-ℤ (x +ℤ y))
( is-nonpositive-neg-is-nonnegative-ℤ
( is-nonnegative-eq-ℤ
( inv (distributive-neg-add-ℤ x y))
( is-nonnegative-neg-is-nonpositive-ℤ H)
( is-nonnegative-neg-is-nonpositive-ℤ K))))


## Definitions

### Addition of positive integers

add-positive-ℤ : positive-ℤ → positive-ℤ → positive-ℤ
add-positive-ℤ (x , H) (y , K) = (add-ℤ x y , is-positive-add-ℤ H K)


### Addition of nonnegative integers

add-nonnegative-ℤ : nonnegative-ℤ → nonnegative-ℤ → nonnegative-ℤ
add-nonnegative-ℤ (x , H) (y , K) = (add-ℤ x y , is-nonnegative-add-ℤ H K)


### Addition of negative integers

add-negative-ℤ : negative-ℤ → negative-ℤ → negative-ℤ
add-negative-ℤ (x , H) (y , K) = (add-ℤ x y , is-negative-add-ℤ H K)


### Addition of nonpositive integers

add-nonpositive-ℤ : nonpositive-ℤ → nonpositive-ℤ → nonpositive-ℤ
add-nonpositive-ℤ (x , H) (y , K) = (add-ℤ x y , is-nonpositive-add-ℤ H K)