From 9c14e7c439fdb478923fefbd7ef0aa30442e687c Mon Sep 17 00:00:00 2001
From: Patrick Stevens <patrick@patrickstevens.co.uk>
Date: Thu, 22 Aug 2019 08:37:41 +0100
Subject: [PATCH] Split out Integers and remove use of K (#39)

---
 Everything/Safe.agda                 |    2 +
 Everything/WithK.agda                |    1 -
 Groups/Examples/ExampleSheet1.agda   |    2 +-
 Groups/Groups2.agda                  |    2 +-
 Groups/LectureNotes/Lecture1.agda    |   11 +-
 Numbers/Integers.agda                | 1574 --------------------------
 Numbers/Integers/Addition.agda       |   95 ++
 Numbers/Integers/Definition.agda     |   35 +
 Numbers/Integers/Integers.agda       |   17 +
 Numbers/Integers/Multiplication.agda |  199 ++++
 Numbers/Integers/Order.agda          |   99 ++
 Numbers/Rationals.agda               |    2 +-
 Numbers/RationalsLemmas.agda         |    2 +-
 Rings/Examples/Examples.agda         |    2 +-
 Rings/Examples/Proofs.agda           |    2 +-
 15 files changed, 462 insertions(+), 1583 deletions(-)
 delete mode 100644 Numbers/Integers.agda
 create mode 100644 Numbers/Integers/Addition.agda
 create mode 100644 Numbers/Integers/Definition.agda
 create mode 100644 Numbers/Integers/Integers.agda
 create mode 100644 Numbers/Integers/Multiplication.agda
 create mode 100644 Numbers/Integers/Order.agda

diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index cb002a0..2c9d3b7 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -5,6 +5,8 @@
 open import Numbers.Naturals.Naturals
 open import Numbers.BinaryNaturals.Definition
 
+open import Numbers.Integers.Integers
+
 open import Lists.Lists
 
 open import Groups.Groups
diff --git a/Everything/WithK.agda b/Everything/WithK.agda
index fef8285..d391630 100644
--- a/Everything/WithK.agda
+++ b/Everything/WithK.agda
@@ -3,7 +3,6 @@
 -- This file contains everything that is --safe, but uses K.
 
 open import PrimeNumbers
-open import Numbers.Integers
 open import Numbers.Rationals
 open import Numbers.RationalsLemmas
 open import Numbers.BinaryNaturals.Multiplication -- TODO there's no reason for this to need K
diff --git a/Groups/Examples/ExampleSheet1.agda b/Groups/Examples/ExampleSheet1.agda
index f9a83ed..b123b44 100644
--- a/Groups/Examples/ExampleSheet1.agda
+++ b/Groups/Examples/ExampleSheet1.agda
@@ -5,7 +5,7 @@ open import Setoids.Setoids
 open import Functions
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Numbers.Naturals.Naturals
-open import Numbers.Integers
+open import Numbers.Integers.Integers
 open import Sets.FinSet
 open import Groups.Definition
 open import Groups.Groups
diff --git a/Groups/Groups2.agda b/Groups/Groups2.agda
index 9045559..8bc33be 100644
--- a/Groups/Groups2.agda
+++ b/Groups/Groups2.agda
@@ -3,7 +3,7 @@
 open import Groups.Groups
 open import Groups.Definition
 open import Orders
-open import Numbers.Integers
+open import Numbers.Integers.Integers
 open import Setoids.Setoids
 open import LogicalFormulae
 open import Sets.FinSet
diff --git a/Groups/LectureNotes/Lecture1.agda b/Groups/LectureNotes/Lecture1.agda
index 8f4d7eb..69d386b 100644
--- a/Groups/LectureNotes/Lecture1.agda
+++ b/Groups/LectureNotes/Lecture1.agda
@@ -5,13 +5,14 @@ open import Setoids.Setoids
 open import Functions
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Numbers.Naturals.Naturals
-open import Numbers.Integers
+open import Numbers.Integers.Integers
 open import Numbers.Rationals
 open import Sets.FinSet
 open import Groups.Definition
 open import Groups.Groups
 open import Rings.Definition
 open import IntegersModN
+open import Semirings.Definition
 
 module Groups.LectureNotes.Lecture1 where
 
@@ -27,13 +28,19 @@ module Groups.LectureNotes.Lecture1 where
   integersMinusNotGroup record { wellDefined = wellDefined ; identity = identity ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with multAssoc {nonneg 3} {nonneg 2} {nonneg 1}
   integersMinusNotGroup record { wellDefined = wellDefined ; identity = identity ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | ()
 
+  negSuccInjective : {a b : ℕ} → (negSucc a ≡ negSucc b) → a ≡ b
+  negSuccInjective {a} {.a} refl = refl
+
+  nonnegInjective : {a b : ℕ} → (nonneg a ≡ nonneg b) → a ≡ b
+  nonnegInjective {a} {.a} refl = refl
+
   integersTimesNotGroup : Group (reflSetoid ℤ) (_*Z_) → False
   integersTimesNotGroup record { wellDefined = wellDefined ; identity = (nonneg zero) ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with multIdentLeft {negSucc 1}
   ... | ()
   integersTimesNotGroup record { wellDefined = wellDefined ; identity = (nonneg (succ zero)) ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with invLeft {nonneg zero}
   ... | bl with inverse (nonneg zero)
   integersTimesNotGroup record { wellDefined = wellDefined ; identity = (nonneg (succ zero)) ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | () | nonneg zero
-  integersTimesNotGroup record { wellDefined = wellDefined ; identity = (nonneg (succ zero)) ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | () | nonneg (succ x)
+  integersTimesNotGroup record { wellDefined = wellDefined ; identity = (nonneg (succ zero)) ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | p | nonneg (succ x) = naughtE (nonnegInjective (transitivity (applyEquality nonneg (equalityCommutative (Semiring.productZeroRight ℕSemiring x))) p))
   integersTimesNotGroup record { wellDefined = wellDefined ; identity = (nonneg (succ zero)) ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | () | negSucc x
   integersTimesNotGroup record { wellDefined = wellDefined ; identity = (nonneg (succ (succ x))) ; inverse = inverse ; multAssoc = multAssoc ; multIdentRight = multIdentRight ; multIdentLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with succInjective (negSuccInjective (multIdentLeft {negSucc 1}))
   ... | ()
diff --git a/Numbers/Integers.agda b/Numbers/Integers.agda
deleted file mode 100644
index e274d23..0000000
--- a/Numbers/Integers.agda
+++ /dev/null
@@ -1,1574 +0,0 @@
-{-# OPTIONS --safe --warning=error #-}
-
-open import LogicalFormulae
-open import Numbers.Naturals.Naturals
-open import Numbers.Naturals.Order -- TODO: remove dependencies on everything other than Naturals.Naturals
-open import Numbers.Naturals.Definition
-open import Numbers.Naturals.Addition
-open import Numbers.Naturals.WithK -- TODO: remove this dependency, it's baked into ZSimple
-open import Groups.Groups
-open import Groups.Definition
-open import Rings.Definition
-open import Functions
-open import Orders
-open import Setoids.Setoids
-open import Setoids.Orders
-open import Rings.IntegralDomains
-open import Semirings.Definition
-
-module Numbers.Integers where
-
-data ℤ : Set where
-  nonneg : ℕ → ℤ
-  negSucc : ℕ → ℤ
-
-data ℤSimple : Set where
-  negative : (a : ℕ) → (0 <N a) → ℤSimple
-  positive : (a : ℕ) → (0 <N a) → ℤSimple
-  zZero : ℤSimple
-
-convertZ : ℤ → ℤSimple
-convertZ (nonneg zero) = zZero
-convertZ (nonneg (succ x)) = positive (succ x) (succIsPositive x)
-convertZ (negSucc x) = negative (succ x) (succIsPositive x)
-
-convertZ' : ℤSimple → ℤ
-convertZ' (negative zero (le x ()))
-convertZ' (negative (succ a) x) = negSucc a
-convertZ' (positive a x) = nonneg a
-convertZ' zZero = nonneg zero
-
-zIsZ : (a : ℤ) → convertZ' (convertZ a) ≡ a
-zIsZ (nonneg zero) = refl
-zIsZ (nonneg (succ x)) = refl
-zIsZ (negSucc x) = refl
-
-zIsZ' : (a : ℤSimple) → convertZ (convertZ' a) ≡ a
-zIsZ' (negative zero (le x ()))
-zIsZ' (negative (succ a) x) = help
-  where
-    eq : (succIsPositive a) ≡ x
-    eq = <NRefl {0} {succ a} (succIsPositive a) x
-    help : negative (succ a) (succIsPositive a) ≡ negative (succ a) x
-    help rewrite eq = refl
-zIsZ' (positive zero (le x ()))
-zIsZ' (positive (succ a) x) = help
-  where
-    eq : (succIsPositive a) ≡ x
-    eq = <NRefl {0} {succ a} (succIsPositive a) x
-    help : positive (succ a) (succIsPositive a) ≡ positive (succ a) x
-    help rewrite eq = refl
-zIsZ' zZero = refl
-
-posIsPos : {a : ℕ} → (pr1 pr2 : 0 <N a) → (positive a pr1 ≡ positive a pr2)
-posIsPos {a} pr1 pr2 rewrite <NRefl pr1 pr2 = refl
-
-negIsNeg : {a : ℕ} → (pr1 pr2 : 0 <N a) → (negative a pr1 ≡ negative a pr2)
-negIsNeg {a} pr1 pr2 rewrite <NRefl pr1 pr2 = refl
-
-infix 15 _+Z_
-_+Z_ : ℤ → ℤ → ℤ
-nonneg zero +Z r = r
-nonneg (succ x) +Z nonneg y = nonneg (succ x +N y)
-nonneg (succ x) +Z negSucc zero = nonneg x
-nonneg (succ x) +Z negSucc (succ a) = nonneg x +Z negSucc a
-negSucc a +Z nonneg zero = negSucc a
-negSucc zero +Z nonneg (succ x) = nonneg x
-negSucc (succ a) +Z nonneg (succ x) = negSucc a +Z nonneg x
-negSucc zero +Z negSucc b = negSucc (succ b)
-negSucc (succ a) +Z negSucc b = negSucc (succ a +N succ b)
-
-depth : ℤSimple → ℕ
-depth (negative a x) = a
-depth (positive a x) = a
-depth zZero = 0
-
-plusZ' : (height : ℕ) → (a : ℤSimple) → (b : ℤSimple) → (depth a +N depth b ≡ height) → ℤSimple
-plusZ' zero (negative zero (le x ())) (negative a₁ x₁) pr
-plusZ' zero (negative (succ a) (le x proof)) (negative a₁ x₁) pr = naughtE (equalityCommutative pr)
-plusZ' zero (negative zero (le x ())) (positive a₁ x₁) pr
-plusZ' zero (negative (succ a) (le x proof)) (positive a₁ x₁) pr = naughtE (equalityCommutative pr)
-plusZ' zero (negative zero (le x ())) zZero pr
-plusZ' zero (negative (succ a) (le x proof)) zZero pr = naughtE (equalityCommutative pr)
-plusZ' zero (positive zero (le x ())) b pr
-plusZ' zero (positive (succ a) x) b pr = naughtE (equalityCommutative pr)
-plusZ' zero zZero (negative zero (le x ())) pr
-plusZ' zero zZero (negative (succ a) x) pr = naughtE (equalityCommutative pr)
-plusZ' zero zZero (positive zero (le x ())) pr
-plusZ' zero zZero (positive (succ a) x) pr = naughtE (equalityCommutative pr)
-plusZ' zero zZero zZero pr = zZero
-plusZ' (succ height) (negative zero (le x ())) b pr
-plusZ' (succ height) (negative (succ a) _) (negative zero (le x ())) pr
-plusZ' (succ height) (negative (succ a) _) (negative (succ b) _) pr = negative (succ a +N succ b) (succIsPositive _)
-plusZ' (succ height) (negative (succ a) _) (positive zero (le x ())) pr
-plusZ' (succ height) (negative (succ zero) _) (positive (succ zero) _) pr = zZero
-plusZ' (succ height) (negative (succ zero) _) (positive (succ (succ b)) _) pr = positive (succ b) (succIsPositive b)
-plusZ' (succ height) (negative (succ (succ a)) _) (positive (succ zero) x) pr = negative (succ a) (succIsPositive a)
-plusZ' (succ zero) (negative (succ (succ a)) _) (positive (succ (succ b)) x) pr = naughtE (equalityCommutative (succInjective pr))
-plusZ' (succ (succ height)) (negative (succ (succ a)) _) (positive (succ (succ b)) x) pr = plusZ' height (negative (succ a) (succIsPositive _)) (positive (succ b) (succIsPositive _)) ans
-  where
-    h : a +N succ (succ b) ≡ height
-    h = succInjective (succInjective pr)
-    ans : succ (a +N succ b) ≡ height
-    ans rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring (succ (succ b)) a = h
-plusZ' (succ height) (negative (succ a) _) zZero pr = negative (succ a) (succIsPositive a)
-plusZ' (succ height) (positive zero (le x ())) b pr
-plusZ' (succ height) (positive (succ a) _) (negative zero (le x ())) pr
-plusZ' (succ height) (positive (succ zero) _) (negative (succ zero) _) pr = zZero
-plusZ' (succ height) (positive (succ zero) _) (negative (succ (succ b)) _) pr = negative (succ b) (succIsPositive b)
-plusZ' (succ height) (positive (succ (succ a)) _) (negative (succ zero) _) pr = positive (succ a) (succIsPositive a)
-plusZ' (succ zero) (positive (succ (succ a)) _) (negative (succ (succ b)) _) pr = naughtE (equalityCommutative (succInjective pr))
-plusZ' (succ (succ height)) (positive (succ (succ a)) _) (negative (succ (succ b)) _) pr = plusZ' height (positive (succ a) (succIsPositive a)) (negative (succ b) (succIsPositive b)) ans
-  where
-    h : a +N succ (succ b) ≡ height
-    h = succInjective (succInjective pr)
-    ans : succ (a +N succ b) ≡ height
-    ans rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring (succ (succ b)) a = h
-plusZ' (succ height) (positive (succ a) _) (positive b x) pr = positive (succ a +N b) (succIsPositive (a +N b))
-plusZ' (succ height) (positive (succ a) _) zZero pr = positive (succ a) (succIsPositive a)
-plusZ' (succ height) zZero b pr = b
-
-infix 15 _+Z'_
-_+Z'_ : ℤSimple → ℤSimple → ℤSimple
-a +Z' b = plusZ' (depth a +N depth b) a b refl
-
-castPlusZ' : {de1 de2 : ℕ} → (r s : ℤSimple) → {pr : depth r +N depth s ≡ de1} → {pr2 : depth r +N depth s ≡ de2} → de1 ≡ de2 → plusZ' de1 r s pr ≡ plusZ' de2 r s pr2
-castPlusZ' {.(depth r +N depth s)} {.(depth r +N depth s)} (r) (s) {refl} {refl} de1=de2 = refl
-
-canKnockOneOff+Z'' : (a b : ℕ) → {pr1 : 0 <N a} → {pr2 : 0 <N b} → {pr3 : 0 <N succ a} → {pr4 : 0 <N succ b} → plusZ' (succ a +N succ b) (positive (succ a) pr3) (negative (succ b) pr4) refl ≡ (plusZ' (a +N b) (positive a pr1) (negative b pr2) refl)
-canKnockOneOff+Z'' zero b {le x ()} {pr2}
-canKnockOneOff+Z'' (succ a) zero {pr1} {le x ()}
-canKnockOneOff+Z'' (succ a) (succ b) {pr1} {pr2} {pr3} {pr4} rewrite <NRefl (succIsPositive a) pr1 | <NRefl (succIsPositive b) pr2 = castPlusZ' {a +N succ (succ b)} {succ (a +N succ b)} (positive (succ a) pr1) (negative (succ b) pr2) help
-  where
-    help : a +N (succ (succ b)) ≡ succ (a +N succ b)
-    help rewrite Semiring.commutative ℕSemiring a (succ (succ b)) | Semiring.commutative ℕSemiring (succ b) a = refl
-
-canKnockOneOff+Z''2 : (a b : ℕ) → {pr1 : 0 <N a} → {pr2 : 0 <N b} → {pr3 : 0 <N succ a} → {pr4 : 0 <N succ b} → plusZ' (succ a +N succ b) (negative (succ a) pr3) (positive (succ b) pr4) refl ≡ (plusZ' (a +N b) (negative a pr1) (positive b pr2) refl)
-canKnockOneOff+Z''2 zero b {le x ()} {pr2}
-canKnockOneOff+Z''2 (succ a) zero {pr1} {le x ()}
-canKnockOneOff+Z''2 (succ a) (succ b) {pr1} {pr2} {pr3} {pr4} rewrite <NRefl (succIsPositive a) pr1 | <NRefl (succIsPositive b) pr2 = castPlusZ' {a +N succ (succ b)} {succ (a +N succ b)} (negative (succ a) pr1) (positive (succ b) pr2) help
-  where
-    help : a +N (succ (succ b)) ≡ succ (a +N succ b)
-    help rewrite Semiring.commutative ℕSemiring a (succ (succ b)) | Semiring.commutative ℕSemiring (succ b) a = refl
-
-lemma' : (x y : ℕ) → succ (x +N succ y) ≡ x +N succ (succ y)
-lemma' x y rewrite Semiring.commutative ℕSemiring x (succ (succ y)) | Semiring.commutative ℕSemiring (succ y) x = refl
-
-helpPlusIsPlus' : (x y : ℕ) → (pr' : _) → negative (succ x) (succIsPositive x) +Z' positive (succ y) (succIsPositive y) ≡ plusZ' (x +N succ (succ y)) (negative (succ x) (logical<NImpliesLe (record {}))) (positive (succ y) (logical<NImpliesLe (record {}))) pr'
-helpPlusIsPlus' x y pr = castPlusZ' {succ x +N succ y} {x +N succ (succ y)} (negative (succ x) (succIsPositive x)) (positive (succ y) (succIsPositive y)) {refl} {pr} pr
-
-helpPlusIsPlus'2 : (x y : ℕ) → (pr' : _) → positive (succ x) (succIsPositive x) +Z' negative (succ y) (succIsPositive y) ≡ plusZ' (succ (x +N succ y)) (positive (succ x) (logical<NImpliesLe (record {}))) (negative (succ y) (logical<NImpliesLe (record {}))) pr'
-helpPlusIsPlus'2 x y pr = castPlusZ' {_} {_} (positive (succ x) (succIsPositive x)) (negative (succ y) (succIsPositive y)) {refl} {pr} pr
-
-canKnockOneOff+Z' : (a b : ℕ) → {pr1 : 0 <N a} → {pr2 : 0 <N b} → {pr3 : 0 <N succ a} → {pr4 : 0 <N succ b} → (positive (succ a) pr3) +Z' (negative (succ b) pr4) ≡ (positive a pr1) +Z' (negative b pr2)
-canKnockOneOff+Z' zero b {le x ()} {pr2} {pr3} {pr4}
-canKnockOneOff+Z' (succ a) zero {pr1} {le x ()} {pr3} {pr4}
-canKnockOneOff+Z' (succ a) (succ b) {pr1} {pr2} {pr3} {pr4} = canKnockOneOff+Z'' (succ a) (succ b) {pr1} {pr2} {pr3} {pr4}
-
-canKnockOneOff+Z'2 : (a b : ℕ) → {pr1 : 0 <N a} → {pr2 : 0 <N b} → {pr3 : 0 <N succ a} → {pr4 : 0 <N succ b} → (negative (succ a) pr3) +Z' (positive (succ b) pr4) ≡ (negative a pr1) +Z' (positive b pr2)
-canKnockOneOff+Z'2 zero b {le x ()} {pr2} {pr3} {pr4}
-canKnockOneOff+Z'2 (succ a) zero {pr1} {le x ()} {pr3} {pr4}
-canKnockOneOff+Z'2 (succ a) (succ b) {pr1} {pr2} {pr3} {pr4} = canKnockOneOff+Z''2 (succ a) (succ b) {pr1} {pr2} {pr3} {pr4}
-
-plusIsPlus' : (a b : ℤ) → convertZ (a +Z b) ≡ (convertZ a) +Z' (convertZ b)
-plusIsPlus' (nonneg zero) (nonneg zero) = refl
-plusIsPlus' (nonneg zero) (nonneg (succ x)) = refl
-plusIsPlus' (nonneg zero) (negSucc x) = refl
-plusIsPlus' (nonneg (succ x)) (nonneg zero) rewrite Semiring.commutative ℕSemiring x 0 = refl
-plusIsPlus' (nonneg (succ x)) (nonneg (succ y)) = refl
-plusIsPlus' (nonneg (succ zero)) (negSucc zero) = refl
-plusIsPlus' (nonneg (succ (succ x))) (negSucc zero) = refl
-plusIsPlus' (nonneg (succ zero)) (negSucc (succ y)) = refl
-plusIsPlus' (nonneg (succ (succ x))) (negSucc (succ y)) rewrite canKnockOneOff+Z' (succ x) (succ y) {succIsPositive x} {succIsPositive y} {succIsPositive (succ x)} {succIsPositive (succ y)} = identityOfIndiscernablesRight _ _ _ _≡_ (plusIsPlus' (nonneg (succ x)) (negSucc y)) (helpPlusIsPlus'2 x y _)
-plusIsPlus' (negSucc x) (nonneg zero) = refl
-plusIsPlus' (negSucc zero) (nonneg (succ zero)) = refl
-plusIsPlus' (negSucc zero) (nonneg (succ (succ y))) = refl
-plusIsPlus' (negSucc (succ x)) (nonneg (succ zero)) = refl
-plusIsPlus' (negSucc (succ x)) (nonneg (succ (succ y))) rewrite equalityCommutative (canKnockOneOff+Z' (succ x) (succ y) {succIsPositive x} {succIsPositive y} {succIsPositive (succ x)} {succIsPositive (succ y)}) = identityOfIndiscernablesRight (convertZ (negSucc x +Z nonneg (succ y))) (negative (succ x) (succIsPositive x) +Z' positive (succ y) (succIsPositive y)) _ _≡_ (plusIsPlus' (negSucc x) (nonneg (succ y))) (helpPlusIsPlus' x y _)
-plusIsPlus' (negSucc zero) (negSucc zero) = refl
-plusIsPlus' (negSucc zero) (negSucc (succ y)) = refl
-plusIsPlus' (negSucc (succ x)) (negSucc y) = refl
-
-plusIsPlusFirstPos : (a : ℕ) (pr1 : 0 <N a) → (b : ℤSimple) → convertZ' ((positive a pr1) +Z' b) ≡ (convertZ' (positive a pr1)) +Z (convertZ' b)
-plusIsPlusFirstPos zero (le x ()) b
-plusIsPlusFirstPos (succ zero) pr1 (negative zero (le x ()))
-plusIsPlusFirstPos (succ zero) pr1 (negative (succ zero) x) = refl
-plusIsPlusFirstPos (succ zero) pr1 (negative (succ (succ b)) x) = refl
-plusIsPlusFirstPos (succ zero) pr1 (positive b x) = refl
-plusIsPlusFirstPos (succ zero) pr1 zZero = refl
-plusIsPlusFirstPos (succ (succ a)) pr1 (negative zero (le x ()))
-plusIsPlusFirstPos (succ (succ a)) pr1 (negative (succ zero) x) = refl
-plusIsPlusFirstPos (succ (succ a)) pr1 (negative (succ (succ b)) x) rewrite canKnockOneOff+Z' (succ a) (succ b) {succIsPositive a} {succIsPositive b} {pr1} {x} = plusIsPlusFirstPos (succ a) (logical<NImpliesLe (record {})) (negative (succ b) (logical<NImpliesLe (record {})))
-plusIsPlusFirstPos (succ (succ a)) pr1 (positive zero (le x ()))
-plusIsPlusFirstPos (succ (succ a)) pr1 (positive (succ zero) x) = refl
-plusIsPlusFirstPos (succ (succ a)) pr1 (positive (succ (succ b)) x) = refl
-plusIsPlusFirstPos (succ (succ a)) pr1 zZero rewrite Semiring.commutative ℕSemiring a 0 = refl
-
-plusIsPlusFirstNeg : (a : ℕ) (pr1 : 0 <N a) → (b : ℤSimple) → convertZ' ((negative a pr1) +Z' b) ≡ (convertZ' (negative a pr1)) +Z (convertZ' b)
-plusIsPlusFirstNeg zero (le x ()) b
-plusIsPlusFirstNeg (succ zero) pr (negative zero (le x ()))
-plusIsPlusFirstNeg (succ zero) pr (negative (succ a) x) = refl
-plusIsPlusFirstNeg (succ zero) pr (positive zero (le x ()))
-plusIsPlusFirstNeg (succ zero) pr (positive (succ zero) x) = refl
-plusIsPlusFirstNeg (succ zero) pr (positive (succ (succ a)) x) = refl
-plusIsPlusFirstNeg (succ zero) pr zZero = refl
-plusIsPlusFirstNeg (succ (succ a)) pr (negative zero (le x ()))
-plusIsPlusFirstNeg (succ (succ a)) pr (negative (succ b) x) = refl
-plusIsPlusFirstNeg (succ (succ a)) pr (positive zero (le x ()))
-plusIsPlusFirstNeg (succ (succ a)) pr (positive (succ zero) x) = refl
-plusIsPlusFirstNeg (succ (succ a)) pr (positive (succ (succ b)) x) rewrite canKnockOneOff+Z'2 (succ a) (succ b) {succIsPositive a} {succIsPositive b} {pr} {x} = plusIsPlusFirstNeg (succ a) (logical<NImpliesLe (record {})) (positive (succ b) (logical<NImpliesLe (record {})))
-plusIsPlusFirstNeg (succ (succ a)) pr zZero = refl
-
-plusIsPlus : (a b : ℤSimple) → convertZ' (a +Z' b) ≡ (convertZ' a) +Z (convertZ' b)
-plusIsPlus (negative a pr) b = plusIsPlusFirstNeg a pr b
-plusIsPlus (positive a pr) b = plusIsPlusFirstPos a pr b
-plusIsPlus zZero (negative zero (le x ()))
-plusIsPlus zZero (negative (succ a) x) = refl
-plusIsPlus zZero (positive zero (le x ()))
-plusIsPlus zZero (positive (succ a) x) = refl
-plusIsPlus zZero zZero = refl
-
-infix 25 _*Z'_
-_*Z'_ : ℤSimple → ℤSimple → ℤSimple
-negative zero (le x ()) *Z' b
-negative (succ a) x *Z' negative zero (le x₁ ())
-negative (succ a) x *Z' negative (succ b) prb = positive (succ a *N succ b) (succIsPositive (b +N a *N succ b))
-negative (succ a) x *Z' positive zero (le x₁ ())
-negative (succ a) x *Z' positive (succ b) prb = negative (succ a *N succ b) (succIsPositive (b +N a *N succ b))
-negative (succ a) x *Z' zZero = zZero
-positive zero (le x ()) *Z' b
-positive (succ a) x *Z' negative zero (le x₁ ())
-positive (succ a) x *Z' negative (succ b) prb = negative (succ a *N succ b) (succIsPositive (b +N a *N succ b))
-positive (succ a) x *Z' positive zero (le x₁ ())
-positive (succ a) x *Z' positive (succ b) prb = positive (succ a *N succ b) (succIsPositive (b +N a *N succ b))
-positive (succ a) x *Z' zZero = zZero
-zZero *Z' b = zZero
-
-infix 25 _*Z_
-_*Z_ : ℤ → ℤ → ℤ
-a *Z b = convertZ' (convertZ a *Z' convertZ b)
-
-convertZ'DistributesOver*Z : (a b : ℤSimple) → convertZ' (a *Z' b) ≡ (convertZ' a) *Z (convertZ' b)
-convertZ'DistributesOver*Z (negative zero (le x ())) (negative b prb)
-convertZ'DistributesOver*Z (negative (succ a) x) (negative zero (le y ()))
-convertZ'DistributesOver*Z (negative (succ a) x) (negative (succ b) prb) = refl
-convertZ'DistributesOver*Z (negative zero (le x ())) (positive b prb)
-convertZ'DistributesOver*Z (negative (succ a) x) (positive zero (le x₁ ()))
-convertZ'DistributesOver*Z (negative (succ a) x) (positive (succ b) prb) = refl
-convertZ'DistributesOver*Z (negative zero (le x ())) zZero
-convertZ'DistributesOver*Z (negative (succ a) x) zZero = refl
-convertZ'DistributesOver*Z (positive zero (le x ())) b
-convertZ'DistributesOver*Z (positive (succ a) x) (negative zero (le x₁ ()))
-convertZ'DistributesOver*Z (positive (succ a) x) (negative (succ b) prb) = refl
-convertZ'DistributesOver*Z (positive (succ a) x) (positive zero (le x₁ ()))
-convertZ'DistributesOver*Z (positive (succ a) x) (positive (succ b) prb) = refl
-convertZ'DistributesOver*Z (positive (succ a) x) zZero = refl
-convertZ'DistributesOver*Z zZero (negative zero (le x ()))
-convertZ'DistributesOver*Z zZero (negative (succ a) x) = refl
-convertZ'DistributesOver*Z zZero (positive zero (le x ()))
-convertZ'DistributesOver*Z zZero (positive (succ a) x) = refl
-convertZ'DistributesOver*Z zZero zZero = refl
-
-infix 5 _<Z_
-record _<Z_ (a : ℤ) (b : ℤ) : Set where
-  constructor le
-  field
-      x : ℕ
-      proof : (nonneg (succ x)) +Z a ≡ b
-
-addingNonnegIsHom : (a b : ℕ) → nonneg a +Z nonneg b ≡ nonneg (a +N b)
-addingNonnegIsHom zero b = refl
-addingNonnegIsHom (succ a) b = refl
-
-multiplyingNonnegIsHom : (a b : ℕ) → nonneg a *Z nonneg b ≡ nonneg (a *N b)
-multiplyingNonnegIsHom zero b = refl
-multiplyingNonnegIsHom (succ a) zero rewrite multiplicationNIsCommutative a 0 = refl
-multiplyingNonnegIsHom (succ a) (succ b) = refl
-
-multiplyWithZero : (a : ℤ) → a *Z nonneg 0 ≡ nonneg 0
-multiplyWithZero (nonneg zero) rewrite multiplyingNonnegIsHom zero zero = refl
-multiplyWithZero (nonneg (succ x)) rewrite multiplyingNonnegIsHom (succ x) zero = refl
-multiplyWithZero (negSucc x) = refl
-
-multiplyWithZero' : (a : ℤ) → nonneg 0 *Z a ≡ nonneg 0
-multiplyWithZero' (nonneg x) = refl
-multiplyWithZero' (negSucc zero) = refl
-multiplyWithZero' (negSucc (succ x)) = refl
-
-nonnegInjective : {a b : ℕ} → (nonneg a ≡ nonneg b) → (a ≡ b)
-nonnegInjective {a} {.a} refl = refl
-
-lessIsPreservedNToZ : {a b : ℕ} → (a <N b) → ((nonneg a) <Z (nonneg b))
-_<Z_.x (lessIsPreservedNToZ {a} {b} (le x proof)) = x
-_<Z_.proof (lessIsPreservedNToZ {a} {.(succ (x +N a))} (le x refl)) = refl
-
-lessIsPreservedNToZConverse : {a b : ℕ} → ((nonneg a) <Z (nonneg b)) → (a <N b)
-lessIsPreservedNToZConverse {a} {b} (le x proof) = le x (nonnegInjective proof)
-
-additionZIsCommutative : (a b : ℤ) → a +Z b ≡ b +Z a
-additionZIsCommutative (nonneg x) (nonneg y) = splitRight
-  where
-    inN : x +N y ≡ y +N x
-    inN = Semiring.commutative ℕSemiring x y
-    inZ : nonneg (x +N y) ≡ nonneg (y +N x)
-    inZ = applyEquality nonneg inN
-    splitLeft : nonneg x +Z nonneg y ≡ nonneg (y +N x)
-    splitLeft = identityOfIndiscernablesLeft (nonneg (x +N y)) (nonneg (y +N x)) (nonneg x +Z nonneg y) _≡_ inZ (equalityCommutative (addingNonnegIsHom x y))
-    splitRight : nonneg x +Z nonneg y ≡ nonneg y +Z nonneg x
-    splitRight = identityOfIndiscernablesRight (nonneg x +Z nonneg y) (nonneg (y +N x)) (nonneg y +Z nonneg x) _≡_ splitLeft (equalityCommutative (addingNonnegIsHom y x))
-
-additionZIsCommutative (nonneg zero) (negSucc a) = refl
-additionZIsCommutative (nonneg (succ x)) (negSucc zero) = refl
-additionZIsCommutative (nonneg (succ x)) (negSucc (succ a)) = additionZIsCommutative (nonneg x) (negSucc a)
-additionZIsCommutative (negSucc zero) (nonneg zero) = refl
-additionZIsCommutative (negSucc (succ a)) (nonneg zero) = refl
-additionZIsCommutative (negSucc zero) (nonneg (succ x)) = refl
-additionZIsCommutative (negSucc (succ a)) (nonneg (succ x)) = additionZIsCommutative (negSucc a) (nonneg x)
-additionZIsCommutative (negSucc zero) (negSucc zero) = refl
-additionZIsCommutative (negSucc zero) (negSucc (succ b)) = applyEquality negSucc i
-  where
-    h : succ b ≡ b +N succ zero
-    h = equalityCommutative (Semiring.commutative ℕSemiring b 1)
-    i : succ (succ b) ≡ succ (b +N succ zero)
-    i = applyEquality succ h
-
-additionZIsCommutative (negSucc (succ a)) (negSucc zero) = applyEquality negSucc i
-  where
-    i : succ (a +N succ zero) ≡ succ (succ a)
-    i = applyEquality succ (Semiring.commutative ℕSemiring a 1)
-
-additionZIsCommutative (negSucc (succ a)) (negSucc (succ b)) = applyEquality negSucc (applyEquality succ j)
-  where
-    m : succ (a +N b) ≡ succ (b +N a)
-    m = applyEquality succ (Semiring.commutative ℕSemiring a b)
-    r : a +N succ b ≡ b +N succ a
-    r = transitivity (succExtracts a b) (transitivity m (equalityCommutative (succExtracts b a)))
-    k : succ (a +N succ b) ≡ succ (b +N succ a)
-    k rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring b a | Semiring.commutative ℕSemiring (succ a) b = refl
-    j : a +N succ (succ b) ≡ b +N succ (succ a)
-    j = transitivity (succExtracts a (succ b)) (transitivity k (equalityCommutative (succExtracts b (succ a))))
-
-additiveInverseExists : (a : ℕ) → (negSucc a +Z nonneg (succ a)) ≡ nonneg 0
-additiveInverseExists zero = refl
-additiveInverseExists (succ a) = additiveInverseExists a
-
-multiplicationZ'IsCommutative : (a b : ℤSimple) → (a *Z' b ≡ b *Z' a)
-multiplicationZ'IsCommutative (negative zero (le x ())) (negative b prb)
-multiplicationZ'IsCommutative (negative (succ a) _) (negative zero (le x ()))
-multiplicationZ'IsCommutative (negative (succ a) x) (negative (succ b) prb) = res (succIsPositive (b +N a *N succ b)) (succIsPositive (a +N b *N succ a))
-  where
-    h : succ a *N succ b ≡ succ b *N succ a
-    h = multiplicationNIsCommutative (succ a) (succ b)
-    res : (pr1 : 0 <N succ b +N a *N succ b) → (pr2 : 0 <N succ a +N b *N succ a) → positive (succ a *N succ b) pr1 ≡ positive (succ b *N succ a) pr2
-    res pr1 pr2 rewrite h = posIsPos pr1 pr2
-multiplicationZ'IsCommutative (negative zero (le x ())) (positive b prb)
-multiplicationZ'IsCommutative (negative (succ a) x) (positive zero (le _ ()))
-multiplicationZ'IsCommutative (negative (succ a) x) (positive (succ b) prb) = res (succIsPositive (b +N a *N succ b)) (succIsPositive (a +N b *N succ a))
-  where
-    h : succ a *N succ b ≡ succ b *N succ a
-    h = multiplicationNIsCommutative (succ a) (succ b)
-    res : (pr1 : 0 <N succ b +N a *N succ b) → (pr2 : 0 <N succ a +N b *N succ a) → negative (succ a *N succ b) pr1 ≡ negative (succ b *N succ a) pr2
-    res pr1 pr2 rewrite h = negIsNeg pr1 pr2
-multiplicationZ'IsCommutative (negative zero (le x ())) zZero
-multiplicationZ'IsCommutative (negative (succ a) x) zZero = refl
-multiplicationZ'IsCommutative (positive zero (le x ())) (negative b prb)
-multiplicationZ'IsCommutative (positive (succ a) x) (negative zero (le _ ()))
-multiplicationZ'IsCommutative (positive (succ a) x) (negative (succ b) prb) = res (succIsPositive (b +N a *N succ b)) (succIsPositive (a +N b *N succ a))
-  where
-    h : succ a *N succ b ≡ succ b *N succ a
-    h = multiplicationNIsCommutative (succ a) (succ b)
-    res : (pr1 : 0 <N succ b +N a *N succ b) → (pr2 : 0 <N succ a +N b *N succ a) → negative (succ a *N succ b) pr1 ≡ negative (succ b *N succ a) pr2
-    res pr1 pr2 rewrite h = negIsNeg pr1 pr2
-multiplicationZ'IsCommutative (positive zero (le x ())) (positive b prb)
-multiplicationZ'IsCommutative (positive (succ a) x) (positive zero (le x₁ ()))
-multiplicationZ'IsCommutative (positive (succ a) _) (positive (succ b) _) = res (succIsPositive (b +N a *N succ b)) (succIsPositive (a +N b *N succ a))
-  where
-    h : succ a *N succ b ≡ succ b *N succ a
-    h = multiplicationNIsCommutative (succ a) (succ b)
-    res : (pr1 : 0 <N succ b +N a *N succ b) → (pr2 : 0 <N succ a +N b *N succ a) → positive (succ a *N succ b) pr1 ≡ positive (succ b *N succ a) pr2
-    res pr1 pr2 rewrite h = posIsPos pr1 pr2
-multiplicationZ'IsCommutative (positive zero (le x ())) zZero
-multiplicationZ'IsCommutative (positive (succ a) x) zZero = refl
-multiplicationZ'IsCommutative zZero (negative zero (le x ()))
-multiplicationZ'IsCommutative zZero (negative (succ a) x) = refl
-multiplicationZ'IsCommutative zZero (positive zero (le x ()))
-multiplicationZ'IsCommutative zZero (positive (succ a) x) = refl
-multiplicationZ'IsCommutative zZero zZero = refl
-
-multiplicationZIsCommutative : (a b : ℤ) → (a *Z b ≡ b *Z a)
-multiplicationZIsCommutative a b = res
-  where
-    help : convertZ' (convertZ a *Z' convertZ b) ≡ convertZ' (convertZ b *Z' convertZ a)
-    help = applyEquality convertZ' (multiplicationZ'IsCommutative (convertZ a) (convertZ b))
-    res : a *Z b ≡ b *Z a
-    res rewrite zIsZ a | zIsZ b = help
-
-negSuccIsNotNonneg : (a b : ℕ) → (negSucc a ≡ nonneg b) → False
-negSuccIsNotNonneg zero b ()
-negSuccIsNotNonneg (succ a) b ()
-
-negSuccInjective : {a b : ℕ} → (negSucc a ≡ negSucc b) → a ≡ b
-negSuccInjective refl = refl
-
-zeroMultInZLeft : (a : ℤ) → (nonneg zero) *Z a ≡ (nonneg zero)
-zeroMultInZLeft a = identityOfIndiscernablesLeft (a *Z nonneg zero) (nonneg zero) (nonneg zero *Z a) _≡_ (multiplyWithZero a) (multiplicationZIsCommutative a (nonneg zero))
-
-additionZeroDoesNothing : (a : ℤ) → (a +Z nonneg zero ≡ a)
-additionZeroDoesNothing (nonneg zero) = refl
-additionZeroDoesNothing (nonneg (succ x)) = applyEquality nonneg (applyEquality succ (addZeroRight x))
-additionZeroDoesNothing (negSucc x) = refl
-
-canSubtractOne : (a : ℤ) (b : ℕ) → negSucc zero +Z a ≡ negSucc (succ b) → a ≡ negSucc b
-canSubtractOne (nonneg zero) b pr = i
-  where
-    simplified : negSucc zero ≡ negSucc (succ b)
-    simplified = identityOfIndiscernablesLeft (negSucc zero +Z nonneg zero) (negSucc (succ b)) (negSucc zero) _≡_ pr refl
-    removeNegsucc : zero ≡ succ b
-    removeNegsucc = negSuccInjective simplified
-    f : False
-    f = succIsNonzero (equalityCommutative removeNegsucc)
-    i : (nonneg zero) ≡ negSucc b
-    i = exFalso f
-canSubtractOne (nonneg (succ x)) b pr = exFalso (negSuccIsNotNonneg (succ b) x (equalityCommutative pr))
-canSubtractOne (negSucc x) .x refl = refl
-
-canAddOne : (a : ℤ) (b : ℕ) → a ≡ negSucc b → negSucc zero +Z a ≡ negSucc (succ b)
-canAddOne (nonneg x) b ()
-canAddOne (negSucc x) .x refl = refl
-
-canAddOneReversed : (a : ℤ) (b : ℕ) → a ≡ negSucc b → a +Z negSucc zero ≡ negSucc (succ b)
-canAddOneReversed a b pr = identityOfIndiscernablesLeft (negSucc zero +Z a) (negSucc (succ b)) (a +Z negSucc zero) _≡_ (canAddOne a b pr) (additionZIsCommutative (negSucc zero) a)
-
-addToNegativeSelf : (a : ℕ) → negSucc a +Z nonneg a ≡ negSucc zero
-addToNegativeSelf zero = refl
-addToNegativeSelf (succ a) = addToNegativeSelf a
-
-multiplicativeIdentityOneZNegsucc : (a : ℕ) → (negSucc a *Z nonneg (succ zero) ≡ negSucc a)
-multiplicativeIdentityOneZNegsucc zero = refl
-multiplicativeIdentityOneZNegsucc (succ x) rewrite multiplicationZIsCommutative (negSucc (succ x)) (nonneg 1) | Semiring.commutative ℕSemiring x 0 = refl
-
-multiplicativeIdentityOneZ : (a : ℤ) → (a *Z nonneg (succ zero) ≡ a)
-multiplicativeIdentityOneZ (nonneg zero) rewrite multiplicationZIsCommutative (nonneg 0) (nonneg 1) = refl
-multiplicativeIdentityOneZ (nonneg (succ x)) rewrite multiplicationZIsCommutative (nonneg (succ x)) (nonneg 1) | Semiring.commutative ℕSemiring x 0 = refl
-multiplicativeIdentityOneZ (negSucc x) = multiplicativeIdentityOneZNegsucc (x)
-
-multiplicativeIdentityOneZLeft : (a : ℤ) → (nonneg (succ zero)) *Z a ≡ a
-multiplicativeIdentityOneZLeft a = identityOfIndiscernablesLeft (a *Z nonneg (succ zero)) a (nonneg (succ zero) *Z a) _≡_ (multiplicativeIdentityOneZ a) (multiplicationZIsCommutative a (nonneg (succ zero)))
-
--- Define the equivalence of negSucc + nonneg = nonneg with the corresponding statements of naturals
-
-negSuccPlusNonnegNonneg : (a : ℕ) → (b : ℕ) → (c : ℕ) → (negSucc a +Z (nonneg b) ≡ nonneg c) → b ≡ c +N succ a
-negSuccPlusNonnegNonneg zero zero c ()
-negSuccPlusNonnegNonneg zero (succ b) .b refl rewrite succExtracts b zero | addZeroRight b = refl
-negSuccPlusNonnegNonneg (succ a) zero c ()
-negSuccPlusNonnegNonneg (succ a) (succ b) c pr with negSuccPlusNonnegNonneg a b c pr
-... | prev = identityOfIndiscernablesRight (succ b) (succ (c +N succ a)) (c +N succ (succ a)) _≡_ (applyEquality succ prev) (equalityCommutative (succExtracts c (succ a)))
-
-negSuccPlusNonnegNonnegConverse : (a : ℕ) → (b : ℕ) → (c : ℕ) → (b ≡ c +N succ a) → (negSucc a +Z (nonneg b) ≡ nonneg c)
-negSuccPlusNonnegNonnegConverse zero zero c pr rewrite succExtracts c zero = naughtE pr
-negSuccPlusNonnegNonnegConverse zero (succ b) c pr rewrite Semiring.commutative ℕSemiring c 1 with succInjective pr
-... | pr' = applyEquality nonneg pr'
-negSuccPlusNonnegNonnegConverse (succ a) zero c pr rewrite succExtracts c (succ a) = naughtE pr
-negSuccPlusNonnegNonnegConverse (succ a) (succ b) c pr rewrite succExtracts c (succ a) with succInjective pr
-... | pr' = negSuccPlusNonnegNonnegConverse a b c pr'
-
--- Define the equivalence of negSucc + nonneg = negSucc with the corresponding statements of naturals
-
-negSuccPlusNonnegNegsucc : (a b c : ℕ) → (negSucc a +Z (nonneg b) ≡ negSucc c) → c +N b ≡ a
-negSuccPlusNonnegNegsucc zero zero .0 refl = refl
-negSuccPlusNonnegNegsucc zero (succ b) c ()
-negSuccPlusNonnegNegsucc (succ a) zero .(succ a) refl rewrite addZeroRight a = refl
-negSuccPlusNonnegNegsucc (succ a) (succ b) c pr with negSuccPlusNonnegNegsucc a b c pr
-... | pr' = identityOfIndiscernablesLeft (succ (c +N b)) (succ a) (c +N succ b) _≡_ (applyEquality succ pr') (equalityCommutative (succExtracts c b))
-
-negSuccPlusNonnegNegsuccConverse : (a b c : ℕ) → (c +N b ≡ a) → (negSucc a +Z (nonneg b) ≡ negSucc c)
-negSuccPlusNonnegNegsuccConverse zero zero c pr rewrite addZeroRight c = applyEquality negSucc (equalityCommutative pr)
-negSuccPlusNonnegNegsuccConverse zero (succ b) c pr rewrite succExtracts c b = naughtE (equalityCommutative pr)
-negSuccPlusNonnegNegsuccConverse (succ a) zero c pr rewrite addZeroRight c = applyEquality negSucc (equalityCommutative pr)
-negSuccPlusNonnegNegsuccConverse (succ a) (succ b) c pr rewrite succExtracts c b = negSuccPlusNonnegNegsuccConverse a b c (succInjective pr)
-
--- Define the impossibility of negSucc + negSucc = nonneg
-negSuccPlusNegSuccIsNegative : (a b c : ℕ) → ((negSucc a) +Z (negSucc b) ≡ nonneg c) → False
-negSuccPlusNegSuccIsNegative zero b c ()
-negSuccPlusNegSuccIsNegative (succ a) b c ()
-
--- Define the equivalence of negSucc + negSucc = negSucc
-negSuccPlusNegSuccNegSucc : (a b c : ℕ) → (negSucc a) +Z (negSucc b) ≡ (negSucc c) → succ (a +N b) ≡ c
-negSuccPlusNegSuccNegSucc zero b .(succ b) refl = refl
-negSuccPlusNegSuccNegSucc (succ a) b .(succ (a +N succ b)) refl = applyEquality succ (equalityCommutative (succExtracts a b))
-
-negSuccPlusNegSuccNegSuccConverse : (a b c : ℕ) → succ (a +N b) ≡ c → (negSucc a) +Z (negSucc b) ≡ negSucc c
-negSuccPlusNegSuccNegSuccConverse zero b c pr = applyEquality negSucc pr
-negSuccPlusNegSuccNegSuccConverse (succ a) b zero ()
-negSuccPlusNegSuccNegSuccConverse (succ a) b (succ c) pr rewrite succExtracts a b = applyEquality negSucc pr
-
--- Define the equivalence of nonneg + nonneg = nonneg
-nonnegPlusNonnegNonneg : (a b c : ℕ) → nonneg a +Z nonneg b ≡ nonneg c → a +N b ≡ c
-nonnegPlusNonnegNonneg a b c pr rewrite addingNonnegIsHom a b = nonnegInj pr
-  where
-    nonnegInj : {x y : ℕ} → (pr : nonneg x ≡ nonneg y) → x ≡ y
-    nonnegInj {x} {.x} refl = refl
-
-nonnegPlusNonnegNonnegConverse : (a b c : ℕ) → a +N b ≡ c → nonneg a +Z nonneg b ≡ nonneg c
-nonnegPlusNonnegNonnegConverse a b c pr rewrite addingNonnegIsHom a b = applyEquality nonneg pr
-
-nonnegIsNotNegsucc : {x y : ℕ} → nonneg x ≡ negSucc y → False
-nonnegIsNotNegsucc {x} {y} ()
-
--- Define the impossibility of nonneg + nonneg = negSucc
-nonnegPlusNonnegNegsucc : (a b c : ℕ) → nonneg a +Z nonneg b ≡ negSucc c → False
-nonnegPlusNonnegNegsucc a b c pr rewrite addingNonnegIsHom a b = nonnegIsNotNegsucc pr
-
--- Move negSucc to other side of equation
-moveNegsucc : (a : ℕ) (b c : ℤ) → (negSucc a) +Z b ≡ c → b ≡ c +Z (nonneg (succ a))
-moveNegsucc a (nonneg x) (nonneg y) pr with (negSuccPlusNonnegNonneg a x y pr)
-... | pr' = identityOfIndiscernablesRight (nonneg x) (nonneg (y +N succ a)) (nonneg y +Z nonneg (succ a)) _≡_ (applyEquality nonneg pr') (equalityCommutative (addingNonnegIsHom y (succ a)))
-moveNegsucc a (nonneg x) (negSucc y) pr with negSuccPlusNonnegNegsucc a x y pr
-... | pr' = equalityCommutative (negSuccPlusNonnegNonnegConverse y (succ a) x (g {a} {x} {y} (applyEquality succ pr')))
-  where
-    g : {a x y : ℕ} → succ (y +N x) ≡ succ a → succ a ≡ x +N succ y
-    g {a} {x} {y} p rewrite Semiring.commutative ℕSemiring y x | succExtracts x y = equalityCommutative p
-moveNegsucc a (negSucc x) (nonneg y) pr = exFalso (negSuccPlusNegSuccIsNegative a x y pr)
-moveNegsucc a (negSucc x) (negSucc y) pr with negSuccPlusNegSuccNegSucc a x y pr
-... | pr' = equalityCommutative (negSuccPlusNonnegNegsuccConverse y (succ a) x g)
-  where
-    g : x +N succ a ≡ y
-    g rewrite succExtracts x a | Semiring.commutative ℕSemiring a x = pr'
-
-moveNegsuccConverse : (a : ℕ) → (b c : ℤ) → (b ≡ c +Z (nonneg (succ a))) → (negSucc a) +Z b ≡ c
-moveNegsuccConverse zero (nonneg x) (nonneg y) pr with nonnegPlusNonnegNonneg y 1 x (equalityCommutative pr)
-... | pr' rewrite (equalityCommutative (succIsAddOne y)) = g
-  where
-    g : negSucc 0 +Z nonneg x ≡ nonneg y
-    g rewrite equalityCommutative pr' = refl
-moveNegsuccConverse zero (nonneg x) (negSucc y) pr with moveNegsucc y (nonneg 1) (nonneg x) (equalityCommutative pr)
-... | pr' rewrite addingNonnegIsHom x (succ y) = g x y (nonnegInjective pr')
-  where
-    g : (x y : ℕ) → (1 ≡ (x +N succ y)) → negSucc 0 +Z nonneg x ≡ negSucc y
-    g zero zero pr = refl
-    g zero (succ y) ()
-    g (succ x) y pr = naughtE (identityOfIndiscernablesRight zero (x +N succ y) (succ (x +N y)) _≡_ (succInjective pr) (succExtracts x y))
-moveNegsuccConverse zero (negSucc x) (nonneg y) pr = exFalso (nonnegPlusNonnegNegsucc y 1 x (equalityCommutative pr))
-moveNegsuccConverse zero (negSucc x) (negSucc y) pr with negSuccPlusNonnegNegsucc y 1 x (equalityCommutative pr)
-... | pr' = applyEquality negSucc g
-  where
-    g : succ x ≡ y
-    g rewrite Semiring.commutative ℕSemiring x 1 = pr'
-moveNegsuccConverse (succ a) (nonneg x) (nonneg y) pr with nonnegPlusNonnegNonneg y (succ (succ a)) x (equalityCommutative pr)
-... | pr' = negSuccPlusNonnegNonnegConverse (succ a) x y (equalityCommutative pr')
-moveNegsuccConverse (succ a) (nonneg x) (negSucc y) pr with negSuccPlusNonnegNonneg y (succ (succ a)) x (equalityCommutative pr)
-... | pr' = negSuccPlusNonnegNegsuccConverse (succ a) x y (g a x y pr')
-  where
-    g : (a x y : ℕ) → succ (succ a) ≡ x +N succ y → y +N x ≡ succ a
-    g a x y pr rewrite succExtracts x y | Semiring.commutative ℕSemiring x y = equalityCommutative (succInjective pr)
-moveNegsuccConverse (succ a) (negSucc x) (nonneg z) pr = exFalso (nonnegPlusNonnegNegsucc z (succ (succ a)) x (equalityCommutative pr))
-moveNegsuccConverse (succ a) (negSucc x) (negSucc z) pr with negSuccPlusNonnegNegsucc z (succ (succ a)) x (equalityCommutative pr)
-... | pr' = applyEquality negSucc (g a x z pr')
-  where
-    g : (a x z : ℕ) → x +N succ (succ a) ≡ z → succ (a +N succ x) ≡ z
-    g a x z pr rewrite succExtracts x (succ a) = identityOfIndiscernablesLeft (succ (x +N succ a)) z (succ (a +N succ x)) _≡_ pr (applyEquality succ (s x a))
-      where
-        s : (x a : ℕ) → x +N succ a ≡ a +N succ x
-        s x a rewrite succCanMove a x = Semiring.commutative ℕSemiring x (succ a)
-
--- By this point, any statement about addition can be moved from N into Z and from Z into N by applying moveNegSucc and its converse to eliminate any adding of negSucc.
-
-lessIsPreservedNToZNegsucc : {a b : ℕ} → (a <N b) → ((negSucc b) <Z negSucc a)
-lessIsPreservedNToZNegsucc {a} {b} (le x proof) = record { x = x ; proof = pr }
-  where
-    pr : nonneg (succ x) +Z negSucc b ≡ negSucc a
-    pr rewrite additionZIsCommutative (nonneg (succ x)) (negSucc b) = moveNegsuccConverse b (nonneg (succ x)) (negSucc a) (equalityCommutative (moveNegsuccConverse a (nonneg (succ b)) (nonneg (succ x)) (applyEquality nonneg (applyEquality succ proof'))))
-      where
-        proof' : b ≡ x +N succ a
-        proof' rewrite Semiring.commutative ℕSemiring x a | Semiring.commutative ℕSemiring (succ a) x = equalityCommutative proof
-
-lessLemma : (a x : ℕ) → succ x +N a ≡ a → False
-lessLemma zero x pr = naughtE (equalityCommutative pr)
-lessLemma (succ a) x pr = lessLemma a x q
-  where
-    q : succ x +N a ≡ a
-    q rewrite Semiring.commutative ℕSemiring a (succ x) | Semiring.commutative ℕSemiring x a | Semiring.commutative ℕSemiring (succ a) x = succInjective pr
-
-sumOfNegsucc : (a b : ℕ) → (negSucc a +Z negSucc b) ≡ negSucc (succ (a +N b))
-sumOfNegsucc a b = negSuccPlusNegSuccNegSuccConverse a b (succ (a +N b)) refl
-
-additionZInjLemma : {a b c : ℕ} → (nonneg a ≡ (nonneg a +Z nonneg b) +Z nonneg (succ c)) → False
-additionZInjLemma {a} {b} {c} pr = cannotAddKeepingEquality a (c +N b) pr2''
-  where
-    pr'' : nonneg a ≡ nonneg (a +N b) +Z nonneg (succ c)
-    pr'' = identityOfIndiscernablesRight (nonneg a) ((nonneg a +Z nonneg b) +Z nonneg (succ c)) (nonneg (a +N b) +Z nonneg (succ c)) _≡_ pr (applyEquality (λ i → i +Z nonneg (succ c)) (addingNonnegIsHom a b))
-    pr''' : nonneg a ≡ nonneg ((a +N b) +N succ c)
-    pr''' = identityOfIndiscernablesRight (nonneg a) (nonneg (a +N b) +Z nonneg (succ c)) (nonneg ((a +N b) +N succ c)) _≡_ pr'' (addingNonnegIsHom (a +N b) (succ c))
-    pr2 : a ≡ (a +N b) +N succ c
-    pr2 = nonnegInjective pr'''
-    pr2' : a ≡ a +N (b +N succ c)
-    pr2' = identityOfIndiscernablesRight a ((a +N b) +N succ c) (a +N (b +N succ c)) _≡_ pr2 (additionNIsAssociative a b (succ c))
-    pr2'' : a ≡ a +N succ (c +N b)
-    pr2'' rewrite Semiring.commutative ℕSemiring (succ c) b = pr2'
-
-additionZInjectiveFirstLemma : (a : ℕ) → (b c : ℤ) → (nonneg a +Z b ≡ nonneg a +Z c) → (b ≡ c)
-additionZInjectiveFirstLemma a (nonneg b) (nonneg c) pr rewrite (addingNonnegIsHom a b) | (addingNonnegIsHom a c) = applyEquality nonneg (canSubtractFromEqualityLeft {a} pr')
-  where
-    pr' : a +N b ≡ a +N c
-    pr' = nonnegInjective pr
-additionZInjectiveFirstLemma a (nonneg b) (negSucc c) pr = exFalso (additionZInjLemma pr')
-  where
-    pr' : nonneg a ≡ (nonneg a +Z nonneg b) +Z nonneg (succ c)
-    pr' rewrite additionZIsCommutative (nonneg a) (negSucc c) = moveNegsucc c (nonneg a) (nonneg a +Z nonneg b) (equalityCommutative pr)
-additionZInjectiveFirstLemma a (negSucc b) (nonneg x) pr = exFalso (additionZInjLemma pr')
-  where
-    pr' : nonneg a ≡ (nonneg a +Z nonneg x) +Z nonneg (succ b)
-    pr' rewrite additionZIsCommutative (nonneg a) (negSucc b) = moveNegsucc b (nonneg a) (nonneg a +Z nonneg x) pr
-additionZInjectiveFirstLemma zero (negSucc zero) (negSucc x) pr = pr
-additionZInjectiveFirstLemma zero (negSucc (succ b)) (negSucc x) pr = pr
-additionZInjectiveFirstLemma (succ a) (negSucc zero) (negSucc x) pr = applyEquality negSucc (equalityCommutative qr'')
-  where
-    pr1 : negSucc x +Z nonneg (succ a) ≡ nonneg a
-    pr1 rewrite additionZIsCommutative (nonneg (succ a)) (negSucc x) = equalityCommutative pr
-    pr' : nonneg a +Z nonneg (succ x) ≡ nonneg (succ a)
-    pr' = equalityCommutative (moveNegsucc x (nonneg (succ a)) (nonneg a) pr1)
-    pr'' : nonneg (a +N succ x) ≡ nonneg (succ a)
-    pr'' rewrite equalityCommutative (addingNonnegIsHom a (succ x)) = pr'
-    pr''' : a +N succ x ≡ succ a
-    pr''' = nonnegInjective pr''
-    pr'''' : succ x +N a ≡ succ a
-    pr'''' rewrite Semiring.commutative ℕSemiring (succ x) a = pr'''
-    qr : succ (a +N x) ≡ succ a
-    qr rewrite Semiring.commutative ℕSemiring a x = pr''''
-    qr' : a +N x ≡ a +N 0
-    qr' rewrite addZeroRight a = succInjective qr
-    qr'' : x ≡ 0
-    qr'' = canSubtractFromEqualityLeft {a} qr'
-additionZInjectiveFirstLemma (succ a) (negSucc (succ b)) (negSucc zero) pr = naughtE qr
-  where
-    pr' : nonneg a ≡ nonneg a +Z nonneg (succ b)
-    pr' rewrite additionZIsCommutative (nonneg a) (negSucc b) = moveNegsucc b (nonneg a) (nonneg a) pr
-    pr'' : nonneg a ≡ nonneg (a +N succ b)
-    pr'' rewrite equalityCommutative (addingNonnegIsHom a (succ b)) = pr'
-    pr''' : a +N 0 ≡ a +N succ b
-    pr''' rewrite addZeroRight a = nonnegInjective pr''
-    qr : 0 ≡ succ b
-    qr = canSubtractFromEqualityLeft {a} pr'''
-additionZInjectiveFirstLemma (succ a) (negSucc (succ b)) (negSucc (succ x)) pr = go b x pr''
-  where
-    pr' : negSucc b ≡ negSucc x
-    pr' = additionZInjectiveFirstLemma a (negSucc b) (negSucc x) pr
-    pr'' : b ≡ x
-    pr'' = negSuccInjective pr'
-    go : (b x : ℕ) → (b ≡ x) → negSucc (succ b) ≡ negSucc (succ x)
-    go b .b refl = refl
-
-additionZInjectiveSecondLemmaLemma : (a : ℕ) (b : ℕ) (c : ℕ) → (negSucc a +Z nonneg b ≡ negSucc a +Z negSucc c) → nonneg b ≡ negSucc c
-additionZInjectiveSecondLemmaLemma zero zero zero pr = naughtE (negSuccInjective pr)
-additionZInjectiveSecondLemmaLemma zero zero (succ c) pr = naughtE (negSuccInjective pr)
-additionZInjectiveSecondLemmaLemma zero (succ b) c pr = exFalso (nonnegIsNotNegsucc pr)
-additionZInjectiveSecondLemmaLemma (succ a) zero c pr = naughtE (canSubtractFromEqualityLeft {succ a} pr')
-  where
-    pr' : succ a +N zero ≡ succ a +N succ c
-    pr' rewrite addZeroRight (succ a) = negSuccInjective pr
-additionZInjectiveSecondLemmaLemma (succ a) (succ b) c pr = naughtE r
-  where
-    pr' : negSucc (succ (a +N succ c)) +Z nonneg (succ a) ≡ nonneg b
-    pr' = equalityCommutative (moveNegsucc a (nonneg b) (negSucc (succ (a +N succ c))) pr)
-    pr'' : nonneg (succ a) ≡ nonneg b +Z nonneg (succ (succ (a +N succ c)))
-    pr'' = moveNegsucc (succ (a +N succ c)) (nonneg (succ a)) (nonneg b) pr'
-    pr''' : nonneg (succ a) ≡ nonneg (b +N succ (succ (a +N succ c)))
-    pr''' rewrite equalityCommutative (addingNonnegIsHom b (succ (succ (a +N succ c)))) = pr''
-    pr'''' : succ a ≡ b +N ((succ (succ a)) +N succ c)
-    pr'''' = nonnegInjective pr'''
-    q : succ a ≡ (b +N (succ (succ a))) +N succ c
-    q = identityOfIndiscernablesRight (succ a) (b +N ((succ (succ a)) +N succ c)) ((b +N (succ (succ a))) +N succ c) _≡_ pr'''' (equalityCommutative (additionNIsAssociative b (succ (succ a)) (succ c)))
-    moveSucc : (a b : ℕ) → a +N succ b ≡ succ a +N b
-    moveSucc a b rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring a b = refl
-    q' : succ a ≡ (succ b +N succ a) +N succ c
-    q' = identityOfIndiscernablesRight (succ a) ((b +N succ (succ a)) +N succ c) ((succ b +N succ a) +N succ c) _≡_ q (applyEquality (λ t → t +N succ c) (moveSucc b (succ a)))
-    q'' : succ a ≡ (succ a +N succ b) +N succ c
-    q'' = identityOfIndiscernablesRight (succ a) ((succ b +N succ a) +N succ c) ((succ a +N succ b) +N succ c) _≡_ q' (applyEquality (λ t → t +N succ c) (Semiring.commutative ℕSemiring (succ b) (succ a)))
-    q''' : succ a ≡ succ a +N (succ b +N succ c)
-    q''' rewrite equalityCommutative (additionNIsAssociative (succ a) (succ b) (succ c)) = q''
-    q'''' : succ a +N zero ≡ succ a +N (succ b +N succ c)
-    q'''' rewrite addZeroRight (succ a) = q'''
-    r : zero ≡ succ b +N succ c
-    r = canSubtractFromEqualityLeft {succ a} q''''
-
-additionZInjectiveSecondLemma : (a : ℕ) (b c : ℤ) → (negSucc a +Z b ≡ negSucc a +Z c) → b ≡ c
-additionZInjectiveSecondLemma zero (nonneg zero) (nonneg zero) pr = refl
-additionZInjectiveSecondLemma zero (nonneg zero) (nonneg (succ c)) pr = exFalso (nonnegIsNotNegsucc (equalityCommutative pr))
-additionZInjectiveSecondLemma zero (nonneg (succ b)) (nonneg zero) pr = exFalso (nonnegIsNotNegsucc pr)
-additionZInjectiveSecondLemma zero (nonneg (succ b)) (nonneg (succ c)) pr rewrite additionZIsCommutative (negSucc zero) (nonneg b) | additionZIsCommutative (negSucc zero) (nonneg c) = applyEquality (λ t → nonneg (succ t)) pr'
-  where
-    pr' : b ≡ c
-    pr' = nonnegInjective pr
-additionZInjectiveSecondLemma zero (nonneg zero) (negSucc c) pr = naughtE pr'
-  where
-    pr' : zero ≡ succ c
-    pr' = negSuccInjective pr
-additionZInjectiveSecondLemma zero (negSucc b) (nonneg zero) pr = naughtE (negSuccInjective (equalityCommutative pr))
-additionZInjectiveSecondLemma zero (negSucc b) (nonneg (succ c)) pr = exFalso (nonnegIsNotNegsucc (equalityCommutative pr))
-additionZInjectiveSecondLemma zero (negSucc b) (negSucc c) pr = applyEquality negSucc (succInjective pr')
-  where
-    pr' : succ b ≡ succ c
-    pr' = negSuccInjective pr
-additionZInjectiveSecondLemma zero (nonneg (succ b)) (negSucc c) pr = exFalso (nonnegIsNotNegsucc pr)
-additionZInjectiveSecondLemma (succ a) (nonneg zero) (nonneg zero) pr = refl
-additionZInjectiveSecondLemma (succ a) (nonneg zero) (nonneg (succ c)) pr = exFalso (nonnegIsNotNegsucc pr'')
-  where
-    pr' : nonneg c ≡ negSucc (succ a) +Z nonneg (succ a)
-    pr' = moveNegsucc a (nonneg c) (negSucc (succ a)) (equalityCommutative pr)
-    pr'' : nonneg c ≡ negSucc zero
-    pr'' rewrite equalityCommutative (addToNegativeSelf (succ a)) = pr'
-additionZInjectiveSecondLemma (succ a) (nonneg (succ b)) (nonneg zero) pr = exFalso (nonnegIsNotNegsucc pr'')
-  where
-    pr' : nonneg b ≡ negSucc (succ a) +Z nonneg (succ a)
-    pr' = moveNegsucc a (nonneg b) (negSucc (succ a)) pr
-    pr'' : nonneg b ≡ negSucc zero
-    pr'' rewrite equalityCommutative (addToNegativeSelf (succ a)) = pr'
-additionZInjectiveSecondLemma (succ a) (nonneg (succ b)) (nonneg (succ c)) pr = applyEquality (λ t → nonneg (succ t)) pr''
-  where
-    pr' : nonneg b ≡ nonneg c
-    pr' = additionZInjectiveSecondLemma a (nonneg b) (nonneg c) pr
-    pr'' : b ≡ c
-    pr'' = nonnegInjective pr'
-additionZInjectiveSecondLemma (succ a) (nonneg zero) (negSucc c) pr = naughtE pr''
-  where
-    pr' : succ a +N zero ≡ succ a +N succ c
-    pr' rewrite addZeroRight a = negSuccInjective pr
-    pr'' : zero ≡ succ c
-    pr'' = canSubtractFromEqualityLeft {succ a} pr'
-additionZInjectiveSecondLemma (succ a) (nonneg (succ b)) (negSucc c) pr = additionZInjectiveSecondLemmaLemma (succ a) (succ b) c pr
-additionZInjectiveSecondLemma (succ a) (negSucc b) (nonneg c) pr = equalityCommutative pr'
-  where
-    pr' : nonneg c ≡ negSucc b
-    pr' = additionZInjectiveSecondLemmaLemma (succ a) c b (equalityCommutative pr)
-additionZInjectiveSecondLemma (succ a) (negSucc b) (negSucc c) pr = applyEquality negSucc pr'''
-  where
-    pr' : succ a +N succ b ≡ succ a +N succ c
-    pr' = negSuccInjective pr
-    pr'' : succ b ≡ succ c
-    pr'' = canSubtractFromEqualityLeft {succ a} pr'
-    pr''' : b ≡ c
-    pr''' = succInjective pr''
-
-additionZInjective : (a b c : ℤ) → (a +Z b ≡ a +Z c) → b ≡ c
-additionZInjective (nonneg a) b c pr = additionZInjectiveFirstLemma a b c pr
-additionZInjective (negSucc a) b c pr = additionZInjectiveSecondLemma a b c pr
-
-addNonnegSucc : (a : ℤ) → (b c : ℕ) → (a +Z nonneg b ≡ nonneg c) → a +Z nonneg (succ b) ≡ nonneg (succ c)
-addNonnegSucc (nonneg x) b c pr rewrite addingNonnegIsHom x (succ b) | addingNonnegIsHom x b = applyEquality nonneg g
-  where
-    p : x +N b ≡ c
-    p = nonnegInjective pr
-    g : x +N succ b ≡ succ c
-    g = identityOfIndiscernablesLeft (succ (x +N b)) (succ c) (x +N succ b) _≡_ (applyEquality succ p) (equalityCommutative (succExtracts x b))
-addNonnegSucc (negSucc x) b c pr = negSuccPlusNonnegNonnegConverse x (succ b) (succ c) (applyEquality succ p')
-  where
-    p' : b ≡ c +N succ x
-    p' = negSuccPlusNonnegNonneg x b c pr
-
-addNonnegSuccLemma : (a x d : ℕ) → (negSucc (succ a) +Z nonneg zero ≡ negSucc (succ x) +Z nonneg (succ d)) → negSucc (succ a) +Z nonneg (succ zero) ≡ negSucc (succ x) +Z nonneg (succ (succ d))
-addNonnegSuccLemma a x d pr = s
-  where
-    p' : negSucc (succ a) +Z nonneg (succ x) ≡ nonneg d
-    p' = equalityCommutative (moveNegsucc x (nonneg d) (negSucc (succ a)) (equalityCommutative pr))
-    p'' : nonneg (succ x) ≡ nonneg d +Z nonneg (succ (succ a))
-    p'' = moveNegsucc (succ a) (nonneg (succ x)) (nonneg d) p'
-    p''' : nonneg (succ x) ≡ nonneg (d +N succ (succ a))
-    p''' rewrite equalityCommutative (addingNonnegIsHom d (succ (succ a))) = p''
-    q : succ x ≡ d +N succ (succ a)
-    q = nonnegInjective p'''
-    q' : succ x ≡ succ (succ a) +N d
-    q' rewrite Semiring.commutative ℕSemiring (succ (succ a)) d = q
-    q'' : succ x ≡ succ d +N succ a
-    q'' rewrite Semiring.commutative ℕSemiring d (succ a) = q'
-    q''' : succ x ≡ succ a +N succ d
-    q''' rewrite Semiring.commutative ℕSemiring (succ a) (succ d) = q''
-    r : nonneg (succ x) ≡ nonneg (succ a +N succ d)
-    r = applyEquality nonneg q'''
-    r' : nonneg (succ x) ≡ nonneg (succ a) +Z nonneg (succ d)
-    r' = identityOfIndiscernablesRight (nonneg (succ x)) (nonneg (succ a +N succ d)) (nonneg (succ a) +Z nonneg (succ d)) _≡_ r (addingNonnegIsHom (succ a) (succ d))
-    r'' : nonneg (succ x) ≡ nonneg (succ d) +Z nonneg (succ a)
-    r'' rewrite additionZIsCommutative (nonneg (succ d)) (nonneg (succ a)) = r'
-    r''' : nonneg (succ d) ≡ negSucc a +Z nonneg (succ x)
-    r''' = equalityCommutative (moveNegsuccConverse a (nonneg (succ x)) (nonneg (succ d)) r'')
-    s : negSucc a ≡ negSucc x +Z nonneg (succ d)
-    s = equalityCommutative (moveNegsuccConverse x (nonneg (succ d)) (negSucc a) r''')
-
-addNonnegSucc' : (a b : ℤ) → (c d : ℕ) → (a +Z nonneg c ≡ b +Z nonneg d) → a +Z nonneg (succ c) ≡ b +Z nonneg (succ d)
-addNonnegSucc' a (nonneg x) c d pr rewrite addingNonnegIsHom x (succ d) | addingNonnegIsHom x d | addNonnegSucc a c (x +N d) pr = applyEquality nonneg (equalityCommutative (succExtracts x d))
-addNonnegSucc' (nonneg a) (negSucc x) c d pr = equalityCommutative (moveNegsuccConverse x (nonneg (succ d)) ((nonneg a) +Z nonneg (succ c)) (equalityCommutative q))
-  where
-    p : ((nonneg a) +Z nonneg c) +Z nonneg (succ x) ≡ nonneg d
-    p = equalityCommutative (moveNegsucc x (nonneg d) ((nonneg a) +Z nonneg c) (equalityCommutative pr))
-    p' : nonneg ((a +N c) +N succ x) ≡ nonneg d
-    p' = identityOfIndiscernablesLeft ((nonneg a +Z nonneg c) +Z nonneg (succ x)) (nonneg d) (nonneg ((a +N c) +N succ x)) _≡_ p g
-      where
-        g : (nonneg a +Z nonneg c) +Z nonneg (succ x) ≡ nonneg ((a +N c) +N succ x)
-        g rewrite addingNonnegIsHom a c | addingNonnegIsHom (a +N c) (succ x) = refl
-    p'' : (a +N c) +N succ x ≡ d
-    p'' = nonnegInjective p'
-    p''' : (a +N succ c) +N succ x ≡ succ d
-    p''' = identityOfIndiscernablesLeft (succ (a +N c) +N succ x) (succ d) ((a +N succ c) +N succ x) _≡_ (applyEquality succ p'') g
-      where
-        g : succ ((a +N c) +N succ x) ≡ (a +N succ c) +N succ x
-        g = applyEquality (λ i → i +N succ x) {succ (a +N c)} {a +N succ c} (equalityCommutative (succExtracts a c))
-    q : (nonneg a +Z nonneg (succ c)) +Z nonneg (succ x) ≡ nonneg (succ d)
-    q rewrite (addingNonnegIsHom a (succ c)) | addingNonnegIsHom (a +N succ c) (succ x) = applyEquality nonneg p'''
-
-addNonnegSucc' (negSucc a) (negSucc x) c d pr with (inspect (negSucc x +Z nonneg d))
-addNonnegSucc' (negSucc a) (negSucc x) c d pr | (nonneg int) with≡ p = identityOfIndiscernablesRight (negSucc a +Z nonneg (succ c)) (nonneg (succ int)) (negSucc x +Z nonneg (succ d)) _≡_ (addNonnegSucc (negSucc a) c int (transitivity pr p)) (equalityCommutative (addNonnegSucc (negSucc x) d int p))
-addNonnegSucc' (negSucc zero) (negSucc zero) c d pr | negSucc int with≡ p = additionZInjective (negSucc zero) (nonneg c) (nonneg d) pr
-  where
-    pr' : nonneg c ≡ (negSucc zero +Z nonneg d) +Z nonneg 1
-    pr' = moveNegsucc zero (nonneg c) (negSucc zero +Z nonneg d) pr
-addNonnegSucc' (negSucc zero) (negSucc (succ x)) zero d pr | negSucc int with≡ p = equalityCommutative (moveNegsuccConverse x (nonneg d) (nonneg zero) (equalityCommutative (applyEquality nonneg q')))
-  where
-    pr' : nonneg d ≡ (negSucc zero) +Z (nonneg (succ (succ x)))
-    pr' = moveNegsucc (succ x) (nonneg d) (negSucc zero) (equalityCommutative pr)
-    pr'' : nonneg (succ (succ x)) ≡ nonneg d +Z nonneg 1
-    pr'' = moveNegsucc (zero) (nonneg (succ (succ x))) (nonneg d) (equalityCommutative pr')
-    pr''' : nonneg (succ (succ x)) ≡ nonneg (d +N 1)
-    pr''' rewrite equalityCommutative (addingNonnegIsHom d 1) = pr''
-    pr'''' : succ (succ x) ≡ d +N 1
-    pr'''' = nonnegInjective pr'''
-    q : succ (succ x) ≡ succ d
-    q rewrite Semiring.commutative ℕSemiring 1 d = pr''''
-    q' : succ x ≡ d
-    q' = succInjective q
-addNonnegSucc' (negSucc zero) (negSucc (succ x)) (succ c) zero pr | negSucc int with≡ p = exFalso (nonnegIsNotNegsucc pr)
-addNonnegSucc' (negSucc zero) (negSucc (succ x)) (succ c) (succ d) pr | negSucc int with≡ p = addNonnegSucc' (nonneg zero) (negSucc x) c d pr
-addNonnegSucc' (negSucc (succ a)) (negSucc zero) zero d pr | negSucc int with≡ p = naughtE q'
-  where
-    pr' : negSucc (succ a) +Z nonneg 1 ≡ nonneg d
-    pr' = equalityCommutative (moveNegsucc zero (nonneg d) (negSucc (succ a)) (equalityCommutative pr))
-    pr'' : nonneg 1 ≡ nonneg d +Z nonneg (succ (succ a))
-    pr'' = moveNegsucc (succ a) (nonneg 1) (nonneg d) pr'
-    pr''' : nonneg 1 ≡ nonneg (d +N succ (succ a))
-    pr''' rewrite equalityCommutative (addingNonnegIsHom d (succ (succ a))) = pr''
-    q : 1 ≡ succ (succ a) +N d
-    q rewrite Semiring.commutative ℕSemiring (succ (succ a)) d = nonnegInjective pr'''
-    q' : 0 ≡ succ a +N d
-    q' = succInjective q
-addNonnegSucc' (negSucc (succ a)) (negSucc zero) (succ c) zero pr | negSucc int with≡ p = help
-  where
-    pr' : negSucc zero +Z nonneg (succ a) ≡ nonneg c
-    pr' = equalityCommutative (moveNegsucc a (nonneg c) (negSucc zero) pr)
-    pr'' : nonneg (succ a) ≡ nonneg c +Z nonneg 1
-    pr'' = moveNegsucc zero (nonneg (succ a)) (nonneg c) pr'
-    pr''' : nonneg (succ a) ≡ nonneg (c +N 1)
-    pr''' rewrite equalityCommutative (addingNonnegIsHom c 1) = pr''
-    q : succ a ≡ succ c
-    q rewrite Semiring.commutative ℕSemiring 1 c = nonnegInjective pr'''
-    q' : a ≡ c
-    q' = succInjective q
-    help : negSucc a +Z nonneg (succ c) ≡ nonneg zero
-    help rewrite q' = additiveInverseExists c
-addNonnegSucc' (negSucc (succ a)) (negSucc zero) (succ c) (succ d) pr | negSucc int with≡ p = moveNegsuccConverse a (nonneg (succ c)) (nonneg (succ d)) q'
-  where
-    pr' : nonneg c ≡ nonneg d +Z nonneg (succ a)
-    pr' = moveNegsucc a (nonneg c) (nonneg d) pr
-    pr'' : nonneg c ≡ nonneg (d +N succ a)
-    pr'' rewrite equalityCommutative (addingNonnegIsHom d (succ a)) = pr'
-    pr''' : c ≡ d +N succ a
-    pr''' = nonnegInjective pr''
-    pr'''' : succ c ≡ succ d +N succ a
-    pr'''' = applyEquality succ pr'''
-    q : nonneg (succ c) ≡ nonneg (succ d +N succ a)
-    q = applyEquality nonneg pr''''
-    q' : nonneg (succ c) ≡ nonneg (succ d) +Z nonneg (succ a)
-    q' rewrite addingNonnegIsHom (succ d) (succ a) = q
-addNonnegSucc' (negSucc (succ a)) (negSucc (succ x)) zero zero pr | negSucc int with≡ p = applyEquality negSucc (succInjective (negSuccInjective pr))
-addNonnegSucc' (negSucc (succ a)) (negSucc (succ x)) zero (succ d) pr | negSucc int with≡ p = addNonnegSuccLemma a x d pr
-addNonnegSucc' (negSucc (succ a)) (negSucc (succ x)) (succ c) zero pr | negSucc int with≡ p = equalityCommutative (addNonnegSuccLemma x a c (equalityCommutative pr))
-addNonnegSucc' (negSucc (succ a)) (negSucc (succ x)) (succ c) (succ d) pr | negSucc int with≡ p = addNonnegSucc' (negSucc a) (negSucc x) c d pr
-
-subtractNonnegSucc : (a : ℤ) → (b c : ℕ) → (a +Z nonneg (succ b) ≡ nonneg (succ c)) → a +Z nonneg b ≡ nonneg c
-subtractNonnegSucc (nonneg x) b c pr rewrite addingNonnegIsHom x (succ b) | addingNonnegIsHom x b = applyEquality nonneg g
-  where
-    p : succ (x +N b) ≡ succ c
-    p rewrite succExtracts x b = nonnegInjective pr
-    g : x +N b ≡ c
-    g = succInjective p
-subtractNonnegSucc (negSucc x) b c pr = negSuccPlusNonnegNonnegConverse x b c (succInjective p')
-  where
-    p' : succ b ≡ succ (c +N succ x)
-    p' = negSuccPlusNonnegNonneg x (succ b) (succ c) pr
-
-addNegsuccThenNonneg : (a : ℤ) (b c : ℕ) → (a +Z negSucc b) +Z nonneg (succ (c +N b)) ≡ a +Z nonneg c
-addNegsuccThenNonneg (nonneg zero) zero c rewrite addZeroRight c = refl
-addNegsuccThenNonneg (nonneg (succ x)) zero c rewrite addZeroRight c | addingNonnegIsHom x (succ c) = applyEquality nonneg (succExtracts x c)
-addNegsuccThenNonneg (nonneg zero) (succ b) c = moveNegsuccConverse b (nonneg (c +N succ b)) (nonneg c) (equalityCommutative (addingNonnegIsHom c (succ b)))
-addNegsuccThenNonneg (nonneg (succ x)) (succ b) c with addNegsuccThenNonneg (nonneg x) b c
-... | prev = go
-  where
-    go : (nonneg x +Z negSucc b) +Z nonneg (succ (c +N succ b)) ≡ nonneg (succ (x +N c))
-    go rewrite addingNonnegIsHom x c | succExtracts c b = p
-      where
-        p : (nonneg x +Z negSucc b) +Z nonneg (succ (succ (c +N b))) ≡ nonneg (succ (x +N c))
-        p = addNonnegSucc (nonneg x +Z negSucc b) (succ (c +N b)) (x +N c) prev
-addNegsuccThenNonneg (negSucc x) zero c rewrite addZeroRight c | sumOfNegsucc x 0 | addZeroRight x = refl
-addNegsuccThenNonneg (negSucc x) (succ b) c with addNegsuccThenNonneg (negSucc x) b c
-... | prev = go
-  where
-    p : nonneg c ≡ ((negSucc x +Z negSucc b) +Z nonneg (succ (c +N b))) +Z nonneg (succ x)
-    p = moveNegsucc x (nonneg c) ((negSucc x +Z negSucc b) +Z nonneg (succ (c +N b))) (equalityCommutative prev)
-    go : (negSucc x +Z negSucc (succ b)) +Z nonneg (succ (c +N succ b)) ≡ negSucc x +Z nonneg c
-    go rewrite sumOfNegsucc x (succ b) | succExtracts c b = identityOfIndiscernablesLeft ((negSucc x +Z negSucc b) +Z nonneg (succ (c +N b))) (negSucc x +Z nonneg c) (negSucc (x +N succ b) +Z nonneg (succ (c +N b))) _≡_ prev (applyEquality (λ t → t +Z nonneg (succ (c +N b))) {negSucc x +Z negSucc b} {negSucc (x +N succ b)} (identityOfIndiscernablesRight (negSucc x +Z negSucc b) (negSucc (succ (x +N b))) (negSucc (x +N succ b)) _≡_ (sumOfNegsucc x b) (applyEquality negSucc (equalityCommutative (succExtracts x b)))))
-
-addNonnegThenNonneg : (a : ℤ) (b c : ℕ) → (a +Z nonneg b) +Z nonneg c ≡ a +Z nonneg (b +N c)
-addNonnegThenNonneg (nonneg x) b c rewrite addingNonnegIsHom x b | addingNonnegIsHom x (b +N c) | addingNonnegIsHom (x +N b) c = applyEquality nonneg (additionNIsAssociative x b c)
-addNonnegThenNonneg (negSucc x) b zero rewrite addZeroRight b | additionZeroDoesNothing (negSucc x +Z nonneg b) = refl
-addNonnegThenNonneg (negSucc x) b (succ c) with addNonnegThenNonneg (negSucc x) b c
-... | prev = prev'
-  where
-    prev' : ((negSucc x +Z nonneg b) +Z nonneg (succ c)) ≡ negSucc x +Z nonneg (b +N succ c)
-    prev' rewrite addNonnegSucc' (negSucc x +Z nonneg b) (negSucc x) c (b +N c) prev | succExtracts b c = refl
-
-additionZIsAssociativeFirstAndSecondArgNonneg : (a b : ℕ) (c : ℤ) → (nonneg a +Z (nonneg b +Z c)) ≡ ((nonneg a) +Z nonneg b) +Z c
-additionZIsAssociativeFirstAndSecondArgNonneg zero b c = refl
-additionZIsAssociativeFirstAndSecondArgNonneg (succ a) b (nonneg zero) = i
-  where
-    h : nonneg (succ a) +Z (nonneg b +Z nonneg zero) ≡ nonneg (succ a) +Z nonneg b
-    h = identityOfIndiscernablesLeft (nonneg (succ a) +Z nonneg b) (nonneg (succ a) +Z nonneg b) (nonneg (succ a) +Z (nonneg b +Z nonneg zero)) _≡_ refl (applyEquality (λ r → nonneg (succ a) +Z r) {nonneg b} {nonneg b +Z nonneg zero} (equalityCommutative (additionZeroDoesNothing (nonneg b))))
-    i : nonneg (succ a) +Z (nonneg b +Z nonneg zero) ≡ (nonneg (succ a) +Z nonneg b) +Z nonneg zero
-    i = identityOfIndiscernablesRight (nonneg (succ a) +Z (nonneg b +Z nonneg zero)) (nonneg (succ a) +Z nonneg b) ((nonneg (succ a) +Z nonneg b) +Z nonneg zero) _≡_ h (equalityCommutative (additionZeroDoesNothing (nonneg (succ a) +Z nonneg b)))
-additionZIsAssociativeFirstAndSecondArgNonneg (succ x) zero (nonneg (succ c)) = applyEquality nonneg (applyEquality succ (applyEquality (λ n → n +N succ c) {x} {x +N zero} (equalityCommutative (addZeroRight x))))
-additionZIsAssociativeFirstAndSecondArgNonneg (succ x) (succ b) (nonneg (succ c)) = applyEquality nonneg (applyEquality succ i)
-  where
-    h : x +N (succ b +N succ c) ≡ (x +N succ b) +N succ c
-    h = equalityCommutative (additionNIsAssociative x (succ b) (succ c))
-    i : x +N succ (b +N succ c) ≡ (x +N succ b) +N succ c
-    i = identityOfIndiscernablesLeft (x +N (succ b +N succ c)) ((x +N succ b) +N succ c) (x +N succ (b +N succ c)) _≡_ h refl
-additionZIsAssociativeFirstAndSecondArgNonneg (succ x) zero (negSucc c) rewrite addZeroRight x = refl
-additionZIsAssociativeFirstAndSecondArgNonneg (succ x) (succ b) (negSucc zero) rewrite Semiring.commutative ℕSemiring x b | Semiring.commutative ℕSemiring x (succ b) = refl
-additionZIsAssociativeFirstAndSecondArgNonneg (succ x) (succ b) (negSucc (succ c)) rewrite Semiring.commutative ℕSemiring x (succ b) | Semiring.commutative ℕSemiring b x = additionZIsAssociativeFirstAndSecondArgNonneg (succ x) b (negSucc c)
-
-additionZIsAssociativeFirstArgNonneg : (a : ℕ) (b c : ℤ) → (nonneg a +Z (b +Z c) ≡ ((nonneg a) +Z b) +Z c)
-additionZIsAssociativeFirstArgNonneg zero (nonneg b) c = additionZIsAssociativeFirstAndSecondArgNonneg 0 b c
-additionZIsAssociativeFirstArgNonneg 0 (negSucc b) c = refl
-additionZIsAssociativeFirstArgNonneg (succ a) (nonneg b) c = additionZIsAssociativeFirstAndSecondArgNonneg (succ a) b c
-additionZIsAssociativeFirstArgNonneg (succ x) (negSucc zero) (nonneg 0) rewrite addingNonnegIsHom x zero | addZeroRight x = refl
-additionZIsAssociativeFirstArgNonneg (succ x) (negSucc zero) (nonneg (succ c)) = i
-  where
-    h : nonneg (succ (x +N c)) ≡ nonneg (x +N succ c)
-    s : nonneg (x +N succ c) ≡ nonneg (succ c +N x)
-    t : nonneg (x +N succ c) ≡ nonneg (succ c) +Z nonneg x
-    i : nonneg (succ (x +N c)) ≡ nonneg x +Z nonneg (succ c)
-    h = applyEquality nonneg (equalityCommutative (succExtracts x c))
-    s = applyEquality nonneg (Semiring.commutative ℕSemiring x (succ c))
-    t = transitivity s refl
-    i = transitivity h (equalityCommutative (addingNonnegIsHom x (succ c)))
-additionZIsAssociativeFirstArgNonneg (succ x) (negSucc (succ b)) (nonneg 0) rewrite additionZIsCommutative (nonneg x +Z negSucc b) (nonneg zero) = refl
-additionZIsAssociativeFirstArgNonneg (succ x) (negSucc (succ b)) (nonneg (succ c)) = p
-  where
-    p''' : nonneg x +Z (negSucc b +Z nonneg c) ≡ (nonneg x +Z negSucc b) +Z nonneg c
-    p''' = additionZIsAssociativeFirstArgNonneg x (negSucc b) (nonneg c)
-    p'' : (negSucc b +Z nonneg c) +Z nonneg x ≡ (nonneg x +Z negSucc b) +Z nonneg c
-    p'' = identityOfIndiscernablesLeft (nonneg x +Z (negSucc b +Z nonneg c)) ((nonneg x +Z negSucc b) +Z nonneg c) ((negSucc b +Z nonneg c) +Z nonneg x) _≡_ p''' (additionZIsCommutative (nonneg x) (negSucc b +Z nonneg c))
-    p' : (negSucc b +Z nonneg c) +Z nonneg (succ x) ≡ (nonneg x +Z negSucc b) +Z nonneg (succ c)
-    p' = addNonnegSucc' (negSucc b +Z nonneg c) (nonneg x +Z negSucc b) x c p''
-    p : nonneg (succ x) +Z (negSucc b +Z nonneg c) ≡ (nonneg x +Z negSucc b) +Z nonneg (succ c)
-    p = identityOfIndiscernablesLeft ((negSucc b +Z nonneg c) +Z nonneg (succ x)) ((nonneg x +Z negSucc b) +Z nonneg (succ c)) (nonneg (succ x) +Z (negSucc b +Z nonneg c)) _≡_ p' (additionZIsCommutative (negSucc b +Z nonneg c) (nonneg (succ x)))
-additionZIsAssociativeFirstArgNonneg (succ x) (negSucc zero) (negSucc c) = refl
-additionZIsAssociativeFirstArgNonneg (succ a) (negSucc (succ b)) (negSucc zero) rewrite Semiring.commutative ℕSemiring b 1 | additionZIsCommutative (nonneg a +Z negSucc b) (negSucc 0) = equalityCommutative (moveNegsuccConverse 0 (nonneg a +Z negSucc b) (nonneg a +Z negSucc (succ b)) q'')
-  where
-    q : nonneg 1 +Z (nonneg a +Z negSucc (succ b)) ≡ (nonneg 1 +Z nonneg a) +Z negSucc (succ b)
-    q = additionZIsAssociativeFirstAndSecondArgNonneg 1 a (negSucc (succ b))
-    q' : (nonneg 1 +Z nonneg a) +Z negSucc (succ b) ≡ (nonneg a +Z negSucc (succ b)) +Z nonneg 1
-    q' rewrite additionZIsCommutative (nonneg a +Z negSucc (succ b)) (nonneg 1) = equalityCommutative q
-    q'' : nonneg (succ a) +Z negSucc (succ b) ≡ (nonneg a +Z negSucc (succ b)) +Z nonneg 1
-    q'' rewrite addingNonnegIsHom 1 a = q'
-additionZIsAssociativeFirstArgNonneg (succ a) (negSucc (succ b)) (negSucc (succ c)) = ans
-  where
-    ans : nonneg a +Z negSucc (b +N succ (succ c)) ≡ (nonneg a +Z negSucc b) +Z negSucc (succ c)
-    p :   nonneg a +Z (negSucc b +Z negSucc (succ c)) ≡ (nonneg a +Z negSucc b) +Z negSucc (succ c)
-    p = additionZIsAssociativeFirstArgNonneg a (negSucc b) (negSucc (succ c))
-    p' : negSucc (b +N succ (succ c)) ≡ negSucc b +Z negSucc (succ c)
-    p' rewrite additionZIsCommutative (negSucc b) (negSucc (succ c)) | Semiring.commutative ℕSemiring b (succ (succ c)) | Semiring.commutative ℕSemiring c (succ b) | Semiring.commutative ℕSemiring c b  = refl
-    ans rewrite p' = p
-
-additionZIsAssociative : (a b c : ℤ) → (a +Z (b +Z c)) ≡ (a +Z b) +Z c
-additionZIsAssociative (nonneg a) b c = additionZIsAssociativeFirstArgNonneg a b c
-additionZIsAssociative (negSucc a) (nonneg b) c rewrite additionZIsCommutative (negSucc a) (nonneg b) | additionZIsCommutative (negSucc a) (nonneg b +Z c) = p''
-  where
-    p : (nonneg b +Z c) +Z negSucc a ≡ nonneg b +Z (c +Z negSucc a)
-    p = equalityCommutative (additionZIsAssociativeFirstArgNonneg b c (negSucc a))
-    p' : (nonneg b +Z c) +Z negSucc a ≡ nonneg b +Z (negSucc a +Z c)
-    p' rewrite additionZIsCommutative (negSucc a) c = p
-    p'' : (nonneg b +Z c) +Z negSucc a ≡ (nonneg b +Z negSucc a) +Z c
-    p'' rewrite equalityCommutative (additionZIsAssociativeFirstArgNonneg b (negSucc a) c) = p'
-additionZIsAssociative (negSucc a) (negSucc b) (nonneg c) rewrite additionZIsCommutative (negSucc a +Z negSucc b) (nonneg c) | additionZIsCommutative (negSucc b) (nonneg c) | additionZIsCommutative (negSucc a) (nonneg c +Z negSucc b) = p'
-  where
-    p : (nonneg c +Z negSucc b) +Z negSucc a ≡ nonneg c +Z (negSucc b +Z negSucc a)
-    p = equalityCommutative (additionZIsAssociativeFirstArgNonneg c (negSucc b) (negSucc a))
-    p' : (nonneg c +Z negSucc b) +Z negSucc a ≡ nonneg c +Z (negSucc a +Z negSucc b)
-    p' rewrite additionZIsCommutative (negSucc a) (negSucc b) = p
-additionZIsAssociative (negSucc zero) (negSucc zero) (negSucc c) = refl
-additionZIsAssociative (negSucc zero) (negSucc (succ b)) (negSucc c) = refl
-additionZIsAssociative (negSucc (succ a)) (negSucc zero) (negSucc c) rewrite Semiring.commutative ℕSemiring a 1 | Semiring.commutative ℕSemiring a (succ (succ c)) | Semiring.commutative ℕSemiring a (succ c) = refl
-additionZIsAssociative (negSucc (succ a)) (negSucc (succ b)) (negSucc zero) rewrite Semiring.commutative ℕSemiring b 1 | Semiring.commutative ℕSemiring (succ ((a +N succ (succ b)))) 1 = applyEquality (λ t → negSucc (succ t)) (p (succ (succ b)))
-  where
-    p : (r : ℕ) → a +N succ r ≡ succ (a +N r)
-    p r rewrite Semiring.commutative ℕSemiring a (succ r) | Semiring.commutative ℕSemiring r a = refl
-additionZIsAssociative (negSucc (succ a)) (negSucc (succ b)) (negSucc (succ c)) = applyEquality (λ t → negSucc (succ t)) (equalityCommutative (additionNIsAssociative a (succ (succ b)) (succ (succ c))))
-
-lessZIrreflexive : {a : ℤ} → (a <Z a) → False
-lessZIrreflexive {nonneg a} (le x proof) = lessLemma a x (nonnegInjective proof)
-lessZIrreflexive {negSucc a} (le x proof) = naughtE (equalityCommutative q)
-  where
-    pr' : nonneg (succ x) +Z (negSucc a +Z nonneg (succ a)) ≡ negSucc a +Z nonneg (succ a)
-    pr' rewrite additionZIsAssociative (nonneg (succ x)) (negSucc a) (nonneg (succ a)) = applyEquality (λ t → t +Z nonneg (succ a)) proof
-    pr'' : nonneg (succ x) +Z nonneg 0 ≡ nonneg 0
-    pr'' rewrite equalityCommutative (additiveInverseExists a) = identityOfIndiscernablesLeft (nonneg (succ x) +Z (negSucc a +Z nonneg (succ a))) (negSucc a +Z nonneg (succ a)) (nonneg (succ (x +N zero))) _≡_ pr' q
-      where
-        q : nonneg (succ x) +Z (negSucc a +Z nonneg (succ a)) ≡ nonneg (succ (x +N 0))
-        q rewrite Semiring.commutative ℕSemiring x 0 | additiveInverseExists a | Semiring.commutative ℕSemiring x 0 = refl
-    pr''' : succ x +N 0 ≡ 0
-    pr''' rewrite addingNonnegIsHom (succ x) 0 = nonnegInjective pr''
-    q : succ x ≡ 0
-    q rewrite Semiring.commutative ℕSemiring 0 (succ x) = pr'''
-
-lessNegsuccNonneg : {a b : ℕ} → (negSucc a <Z nonneg b)
-lessNegsuccNonneg {a} {b} = record { x = x ; proof = pr }
-  where
-    x : ℕ
-    x = a +N b
-    pr' : nonneg (succ (a +N b)) ≡ nonneg b +Z nonneg (succ a)
-    pr' rewrite addingNonnegIsHom b (succ a) | Semiring.commutative ℕSemiring b (succ a) = refl
-    pr : nonneg (succ x) +Z negSucc a ≡ nonneg b
-    pr rewrite additionZIsCommutative (nonneg (succ x)) (negSucc a) = moveNegsuccConverse a (nonneg (succ (a +N b))) (nonneg b) pr'
-
-lessThanTotalZ : {a b : ℤ} → ((a <Z b) || (b <Z a)) || (a ≡ b)
-lessThanTotalZ {nonneg a} {nonneg b} with orderIsTotal a b
-lessThanTotalZ {nonneg a} {nonneg b} | inl (inl a<b) = inl (inl (lessIsPreservedNToZ a<b))
-lessThanTotalZ {nonneg a} {nonneg b} | inl (inr b<a) = inl (inr (lessIsPreservedNToZ b<a))
-lessThanTotalZ {nonneg a} {nonneg b} | inr a=b = inr (applyEquality nonneg a=b)
-lessThanTotalZ {nonneg a} {negSucc b} = inl (inr (lessNegsuccNonneg {b} {a}))
-lessThanTotalZ {negSucc a} {nonneg x} = inl (inl (lessNegsuccNonneg {a} {x}))
-lessThanTotalZ {negSucc a} {negSucc b} with orderIsTotal a b
-... | inl (inl a<b) = inl (inr (lessIsPreservedNToZNegsucc a<b))
-... | inl (inr b<a) = inl (inl (lessIsPreservedNToZNegsucc b<a))
-lessThanTotalZ {negSucc a} {negSucc .a} | inr refl = inr refl
-
-negSuccPlusNegsuccIsNegsucc : {a b c : ℕ} → (negSucc a +Z negSucc b ≡ nonneg c) → False
-negSuccPlusNegsuccIsNegsucc {zero} {b} {c} pr = nonnegIsNotNegsucc (equalityCommutative pr)
-negSuccPlusNegsuccIsNegsucc {succ a} {b} {c} pr = nonnegIsNotNegsucc (equalityCommutative pr)
-
-multiplicationZ'IsAssociative : (a b c : ℤSimple) → (a *Z' (b *Z' c)) ≡ ((a *Z' b) *Z' c)
-multiplicationZ'IsAssociative (negative zero (le x ())) b c
-multiplicationZ'IsAssociative (negative (succ a) x) (negative zero (le x₁ ())) c
-multiplicationZ'IsAssociative (negative (succ a) x) (negative (succ b) prb) (negative zero (le x₁ ()))
-multiplicationZ'IsAssociative (negative (succ a) x) (negative ( succ b) prb) (negative (succ c) prc) = res _ _
-  where
-    help : _
-    help = Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c)
-    res : (pr1 : 0 <N succ a *N (succ b *N succ c)) → (pr2 : 0 <N (succ a *N succ b) *N succ c) → negative (succ a *N (succ b *N succ c)) pr1 ≡ negative ((succ a *N succ b) *N succ c) pr2
-    res pr1 pr2 rewrite help = negIsNeg pr1 pr2
-multiplicationZ'IsAssociative (negative (succ a) x) (negative (succ b) prb) (positive zero (le x₁ ()))
-multiplicationZ'IsAssociative (negative (succ a) x) (negative (succ b) prb) (positive (succ c) prc) = res _ _
-  where
-    help : _
-    help = Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c)
-    res : (pr1 : 0 <N succ a *N (succ b *N succ c)) → (pr2 : 0 <N (succ a *N succ b) *N succ c) → positive (succ a *N (succ b *N succ c)) pr1 ≡ positive ((succ a *N succ b) *N succ c) pr2
-    res pr1 pr2 rewrite help = posIsPos pr1 pr2
-multiplicationZ'IsAssociative (negative (succ a) x) (negative (succ b) prb) zZero = refl
-multiplicationZ'IsAssociative (negative (succ a) x) (positive zero (le x₁ ())) c
-multiplicationZ'IsAssociative (negative (succ a) x) (positive (succ b) prb) (negative zero (le x₁ ()))
-multiplicationZ'IsAssociative (negative (succ a) x) (positive (succ b) prb) (negative (succ c) prc) = res _ _
-  where
-    help : _
-    help = Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c)
-    res : (pr1 : 0 <N succ a *N (succ b *N succ c)) → (pr2 : 0 <N (succ a *N succ b) *N succ c) → positive (succ a *N (succ b *N succ c)) pr1 ≡ positive ((succ a *N succ b) *N succ c) pr2
-    res pr1 pr2 rewrite help = posIsPos pr1 pr2
-multiplicationZ'IsAssociative (negative (succ a) x) (positive (succ b) prb) (positive zero (le x₁ ()))
-multiplicationZ'IsAssociative (negative (succ a) x) (positive (succ b) prb) (positive (succ c) prc) = res _ _
-  where
-    help : _
-    help = Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c)
-    res : (pr1 : 0 <N succ a *N (succ b *N succ c)) → (pr2 : 0 <N (succ a *N succ b) *N succ c) → negative (succ a *N (succ b *N succ c)) pr1 ≡ negative ((succ a *N succ b) *N succ c) pr2
-    res pr1 pr2 rewrite help = negIsNeg pr1 pr2
-multiplicationZ'IsAssociative (negative (succ a) x) (positive (succ b) prb) zZero = refl
-multiplicationZ'IsAssociative (negative (succ a) x) zZero c = refl
-multiplicationZ'IsAssociative (positive zero (le x ())) b c
-multiplicationZ'IsAssociative (positive (succ a) x) (negative zero (le y ())) c
-multiplicationZ'IsAssociative (positive (succ a) x) (negative (succ b) prb) (negative zero (le x₁ ()))
-multiplicationZ'IsAssociative (positive (succ a) x) (negative (succ b) prb) (negative (succ c) prc) = res _ _
-  where
-    help : _
-    help = Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c)
-    res : (pr1 : 0 <N succ a *N (succ b *N succ c)) → (pr2 : 0 <N (succ a *N succ b) *N succ c) → positive (succ a *N (succ b *N succ c)) pr1 ≡ positive ((succ a *N succ b) *N succ c) pr2
-    res pr1 pr2 rewrite help = posIsPos pr1 pr2
-multiplicationZ'IsAssociative (positive (succ a) x) (negative (succ b) prb) (positive zero (le x₁ ()))
-multiplicationZ'IsAssociative (positive (succ a) x) (negative (succ b) prb) (positive (succ c) prc) = res _ _
-  where
-    help : _
-    help = Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c)
-    res : (pr1 : 0 <N succ a *N (succ b *N succ c)) → (pr2 : 0 <N (succ a *N succ b) *N succ c) → negative (succ a *N (succ b *N succ c)) pr1 ≡ negative ((succ a *N succ b) *N succ c) pr2
-    res pr1 pr2 rewrite help = negIsNeg pr1 pr2
-multiplicationZ'IsAssociative (positive (succ a) x) (negative (succ b) prb) zZero = refl
-multiplicationZ'IsAssociative (positive (succ a) x) (positive zero (le y ())) c
-multiplicationZ'IsAssociative (positive (succ a) x) (positive (succ b) prb) (negative zero (le x₁ ()))
-multiplicationZ'IsAssociative (positive (succ a) x) (positive (succ b) prb) (negative (succ c) prc) = res _ _
-  where
-    help : _
-    help = Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c)
-    res : (pr1 : 0 <N succ a *N (succ b *N succ c)) → (pr2 : 0 <N (succ a *N succ b) *N succ c) → negative (succ a *N (succ b *N succ c)) pr1 ≡ negative ((succ a *N succ b) *N succ c) pr2
-    res pr1 pr2 rewrite help = negIsNeg pr1 pr2
-multiplicationZ'IsAssociative (positive (succ a) x) (positive (succ b) prb) (positive zero (le x₁ ()))
-multiplicationZ'IsAssociative (positive (succ a) x) (positive (succ b) prb) (positive (succ c) prc) = res _ _
-  where
-    help : _
-    help = Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c)
-    res : (pr1 : 0 <N succ a *N (succ b *N succ c)) → (pr2 : 0 <N (succ a *N succ b) *N succ c) → positive (succ a *N (succ b *N succ c)) pr1 ≡ positive ((succ a *N succ b) *N succ c) pr2
-    res pr1 pr2 rewrite help = posIsPos pr1 pr2
-multiplicationZ'IsAssociative (positive (succ a) x) (positive (succ b) prb) zZero = refl
-multiplicationZ'IsAssociative (positive (succ a) x) zZero c = refl
-multiplicationZ'IsAssociative zZero b c = refl
-
-multiplicationZIsAssociative : (a b c : ℤ) → (a *Z (b *Z c)) ≡ (a *Z b) *Z c
-multiplicationZIsAssociative a b c = ans
-  where
-    inter : convertZ' (convertZ a *Z' (convertZ b *Z' convertZ c)) ≡ convertZ' ((convertZ a *Z' convertZ b) *Z' convertZ c)
-    inter = applyEquality convertZ' (multiplicationZ'IsAssociative (convertZ a) (convertZ b) (convertZ c))
-    ans : a *Z (b *Z c) ≡ (a *Z b) *Z c
-    ans rewrite convertZ'DistributesOver*Z (convertZ a) (convertZ b *Z' convertZ c) | convertZ'DistributesOver*Z (convertZ b) (convertZ c) | convertZ'DistributesOver*Z (convertZ a *Z' convertZ b) (convertZ c) | convertZ'DistributesOver*Z (convertZ a) (convertZ b) | zIsZ c | zIsZ b | zIsZ a | zIsZ' (convertZ b *Z' convertZ c) | zIsZ' (convertZ a *Z' convertZ b) = inter
-
-zeroIsAdditiveIdentityRightZ : (a : ℤ) → (a +Z nonneg zero) ≡ a
-zeroIsAdditiveIdentityRightZ (nonneg x) = identityOfIndiscernablesRight (nonneg x +Z nonneg zero) (nonneg (x +N zero)) (nonneg x) _≡_ (addingNonnegIsHom x zero) ((applyEquality nonneg (addZeroRight x)))
-zeroIsAdditiveIdentityRightZ (negSucc a) = refl
-
-additiveInverseZ : (a : ℤ) → ℤ
-additiveInverseZ (nonneg zero) = nonneg zero
-additiveInverseZ (nonneg (succ x)) = negSucc x
-additiveInverseZ (negSucc a) = nonneg (succ a)
-
-addInverseLeftZ : (a : ℤ) → (additiveInverseZ a +Z a ≡ nonneg zero)
-addInverseLeftZ (nonneg zero) = refl
-addInverseLeftZ (nonneg (succ zero)) = refl
-addInverseLeftZ (nonneg (succ (succ x))) = addInverseLeftZ (nonneg (succ x))
-addInverseLeftZ (negSucc zero) = refl
-addInverseLeftZ (negSucc (succ a)) = addInverseLeftZ (negSucc a)
-
-addInverseRightZ : (a : ℤ) → (a +Z additiveInverseZ a ≡ nonneg zero)
-addInverseRightZ (nonneg zero) = refl
-addInverseRightZ (nonneg (succ zero)) = refl
-addInverseRightZ (nonneg (succ (succ x))) = addInverseRightZ (nonneg (succ x))
-addInverseRightZ (negSucc zero) = refl
-addInverseRightZ (negSucc (succ a)) = addInverseRightZ (negSucc a)
-
-flipSign : (a : ℕ) → negSucc a *Z negSucc 0 ≡ nonneg (succ a)
-flipSign zero = refl
-flipSign (succ a) = ans
-  where
-    help : convertZ (negSucc (succ a)) *Z' convertZ (negSucc 0) ≡ convertZ (nonneg (succ (succ a)))
-    help rewrite multiplicationNIsCommutative a 1 | Semiring.commutative ℕSemiring a 0 = refl
-    help' : convertZ' (convertZ (negSucc (succ a)) *Z' convertZ (negSucc 0)) ≡ convertZ' (convertZ (nonneg (succ (succ a))))
-    help' = applyEquality convertZ' help
-    help'' : convertZ' (convertZ (negSucc (succ a))) *Z (convertZ' (convertZ (negSucc 0))) ≡ nonneg (succ (succ a))
-    help'' rewrite convertZ'DistributesOver*Z (convertZ (negSucc (succ a))) (convertZ (negSucc 0)) | zIsZ (nonneg (succ (succ a))) = help'
-    ans : negSucc (succ a) *Z negSucc 0 ≡ nonneg (succ (succ a))
-    ans rewrite zIsZ (negSucc (succ a)) | zIsZ (negSucc 0) = help''
-
-flipSign' : (a : ℕ) → nonneg (succ a) *Z negSucc 0 ≡ negSucc a
-flipSign' a = ans
-  where
-    inter : negSucc 0 *Z negSucc 0 ≡ nonneg 1
-    inter = refl
-    ans : nonneg (succ a) *Z negSucc 0 ≡ negSucc a
-    ans rewrite inter | multiplicationNIsCommutative a 1 | Semiring.commutative ℕSemiring a 0 = refl
-
-additionZ'IsCommutative : (a b : ℤSimple) → a +Z' b ≡ b +Z' a
-additionZ'IsCommutative a b = ans
-  where
-    help : (convertZ' a) +Z (convertZ' b) ≡ (convertZ' b) +Z (convertZ' a)
-    help = additionZIsCommutative (convertZ' a) (convertZ' b)
-    help' : convertZ ((convertZ' a) +Z (convertZ' b)) ≡ convertZ ((convertZ' b) +Z (convertZ' a))
-    help' = applyEquality convertZ help
-    help'' : convertZ (convertZ' a) +Z' convertZ (convertZ' b) ≡ convertZ (convertZ' b) +Z' convertZ (convertZ' a)
-    help'' rewrite equalityCommutative (plusIsPlus' (convertZ' a) (convertZ' b)) | equalityCommutative (plusIsPlus' (convertZ' b) (convertZ' a)) = help'
-    ans : a +Z' b ≡ b +Z' a
-    ans rewrite equalityCommutative (zIsZ' a) | equalityCommutative (zIsZ' b) = help''
-additionZ'IsAssociative : (a b c : ℤSimple) → (a +Z' (b +Z' c)) ≡ (a +Z' b) +Z' c
-additionZ'IsAssociative a b c = identityOfIndiscernablesRight _ _ _ _≡_ helpV''' (applyEquality (λ t → (a +Z' t) +Z' c) (zIsZ' b))
-  where
-    help  : convertZ (convertZ' a +Z (convertZ' b +Z convertZ' c)) ≡ convertZ ((convertZ' a +Z convertZ' b) +Z convertZ' c)
-    help' : convertZ (convertZ' a) +Z' convertZ (convertZ' b +Z convertZ' c) ≡ convertZ (convertZ' a +Z convertZ' b) +Z' convertZ (convertZ' c)
-    help'' : a +Z' convertZ (convertZ' b +Z convertZ' c) ≡ convertZ (convertZ' a +Z convertZ' b) +Z' convertZ (convertZ' c)
-    help''' : a +Z' (convertZ (convertZ' b) +Z' convertZ (convertZ' c)) ≡ convertZ (convertZ' a +Z convertZ' b) +Z' convertZ (convertZ' c)
-    help'''' : a +Z' (b +Z' (convertZ (convertZ' c))) ≡ convertZ (convertZ' a +Z convertZ' b) +Z' convertZ (convertZ' c)
-    helpV : a +Z' (b +Z' c) ≡ convertZ (convertZ' a +Z convertZ' b) +Z' convertZ (convertZ' c)
-    helpV' : a +Z' (b +Z' c) ≡ convertZ (convertZ' a +Z convertZ' b) +Z' c
-    helpV'' : a +Z' (b +Z' c) ≡ (convertZ (convertZ' a) +Z' convertZ (convertZ' b)) +Z' c
-    helpV''' : a +Z' (b +Z' c) ≡ (a +Z' convertZ (convertZ' b)) +Z' c
-    helpV''' = identityOfIndiscernablesRight _ _ _ _≡_ helpV'' (applyEquality (λ t → ((t +Z' convertZ (convertZ' b)) +Z' c)) (zIsZ' a))
-    helpV'' rewrite equalityCommutative (plusIsPlus' (convertZ' a) (convertZ' b)) = helpV'
-    helpV' = identityOfIndiscernablesRight _ _ _ _≡_ helpV (applyEquality (λ t → convertZ (convertZ' a +Z convertZ' b) +Z' t) (zIsZ' c))
-    helpV = identityOfIndiscernablesLeft _ _ _ _≡_ help'''' (applyEquality (λ t → a +Z' (b +Z' t)) (zIsZ' c))
-    help'''' = identityOfIndiscernablesLeft _ _ _ _≡_ help''' (applyEquality (λ t → a +Z' (t +Z' (convertZ (convertZ' c)))) (zIsZ' b))
-    help''' rewrite equalityCommutative (plusIsPlus' (convertZ' b) (convertZ' c)) = help''
-    help'' = identityOfIndiscernablesLeft (convertZ (convertZ' a) +Z' convertZ (convertZ' b +Z convertZ' c)) _ (a +Z' convertZ (convertZ' b +Z convertZ' c)) _≡_ help' (applyEquality (λ t → t +Z' convertZ (convertZ' b +Z convertZ' c)) (zIsZ' a))
-    help = applyEquality convertZ (additionZIsAssociative (convertZ' a) (convertZ' b) (convertZ' c))
-    help' rewrite equalityCommutative (plusIsPlus' (convertZ' a) (convertZ' b +Z convertZ' c)) | equalityCommutative (plusIsPlus' (convertZ' a +Z convertZ' b) (convertZ' c)) = help
-
-pos+Z'Pos : (a b : ℕ) → {pr : 0 <N a} → {pr2 : 0 <N b} → {pr3 : 0 <N a +N b} → (positive a pr) +Z' (positive b pr2) ≡ positive (a +N b) pr3
-pos+Z'Pos zero b {le x ()} {pr2} {pr3}
-pos+Z'Pos (succ a) zero {pr} {le x ()} {pr3}
-pos+Z'Pos (succ a) (succ b) {pr} {pr2} {pr3} rewrite <NRefl (pr) (succIsPositive a) | <NRefl pr2 (succIsPositive b) | <NRefl pr3 (succIsPositive (a +N succ b)) = refl
-
-lemma'' : (a b c : ℕ) → (pr : _) → (pr2 : _) → (pr3 : _) → positive (succ ((b +N succ c) +N a *N succ (b +N succ c))) pr ≡ positive (succ (b +N a *N succ b)) pr2 +Z' positive (succ (c +N a *N succ c)) pr3
-lemma'' a b c pr1 pr2 pr3 = equalityCommutative help'
-  where
-    pr' : succ (b +N a *N succ b) +N succ (c +N a *N succ c) ≡ succ ((b +N succ c) +N a *N succ (b +N succ c))
-    pr' = equalityCommutative (Semiring.+DistributesOver* ℕSemiring (succ a) (succ b) (succ c))
-    pr'' : 0 <N succ (b +N a *N succ b) +N succ (c +N a *N succ c)
-    pr'' rewrite pr' = pr1
-    help : (positive (succ (b +N a *N succ b))) pr2 +Z' (positive (succ (c +N a *N succ c))) pr3 ≡ positive (succ (b +N a *N succ b) +N succ (c +N a *N succ c)) pr''
-    help = pos+Z'Pos (succ (b +N a *N succ b)) (succ (c +N a *N succ c)) {pr2} {pr3} {pr''}
-    help' : (positive (succ (b +N a *N succ b))) pr2 +Z' (positive (succ (c +N a *N succ c))) pr3 ≡ positive (succ ((b +N succ c) +N a *N succ (b +N succ c))) pr1
-    help' rewrite equalityCommutative pr' | <NRefl pr1 (succIsPositive ((b +N a *N succ b) +N succ (c +N a *N succ c))) = refl
-
-addZZero : (a : ℤSimple) → a +Z' zZero ≡ a
-addZZero (negative zero (le x ()))
-addZZero (negative (succ a) x) rewrite additionZ'IsCommutative (negative (succ a) x) zZero = refl
-addZZero (positive zero (le x ()))
-addZZero (positive (succ a) x) rewrite additionZ'IsCommutative (positive (succ a) x) zZero = refl
-addZZero zZero = refl
-
-negSucc+ZNegSucc : (a b : ℕ) → (negSucc a +Z negSucc b) ≡ negSucc (succ a +N b)
-negSucc+ZNegSucc zero b = refl
-negSucc+ZNegSucc (succ a) b rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring b a = refl
-
-oneIsIdentity : (a : ℤ) → convertZ' (positive 1 (succIsPositive 0) *Z' convertZ a) ≡ a
-oneIsIdentity (nonneg zero) = refl
-oneIsIdentity (nonneg (succ x)) rewrite Semiring.commutative ℕSemiring x 0 = refl
-oneIsIdentity (negSucc x) rewrite Semiring.commutative ℕSemiring x 0 = refl
-
-oneIsIdentity' : (a : ℤSimple) → (positive 1 (succIsPositive 0)) *Z' a ≡ a
-oneIsIdentity' (negative zero (le x ()))
-oneIsIdentity' (negative (succ a) x) rewrite Semiring.commutative ℕSemiring a 0 | <NRefl x (logical<NImpliesLe (record {})) = refl
-oneIsIdentity' (positive zero (le x ()))
-oneIsIdentity' (positive (succ a) x) rewrite Semiring.commutative ℕSemiring a 0 | <NRefl x (logical<NImpliesLe (record {})) = refl
-oneIsIdentity' zZero = refl
-
-canPullOutSuccZ' : (a : ℕ) → (b c : ℤSimple) → (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ (b +Z' c) +Z' (positive (succ a) (succIsPositive a)) *Z' (b +Z' c)
-canPullOutSuccZ' a (negative zero (le x ())) c
-canPullOutSuccZ' a (negative (succ b) _) (negative zero (le x ()))
-canPullOutSuccZ' a (negative (succ b) _) (negative (succ c) x) = refl
-canPullOutSuccZ' a (negative (succ b) _) (positive zero (le x ()))
-canPullOutSuccZ' a (negative (succ b) y) (positive (succ c) x) with negative (succ b) y +Z' positive (succ c) x
-canPullOutSuccZ' a (negative (succ b) y) (positive (succ c) x) | negative zero (le x₁ ())
-canPullOutSuccZ' a (negative (succ b) y) (positive (succ c) x) | negative (succ sum) pr = refl
-canPullOutSuccZ' a (negative (succ b) y) (positive (succ c) x) | positive zero (le x₁ ())
-canPullOutSuccZ' a (negative (succ b) y) (positive (succ c) x) | positive (succ sum) pr = refl
-canPullOutSuccZ' a (negative (succ b) y) (positive (succ c) x) | zZero = refl
-canPullOutSuccZ' a (negative (succ b) _) zZero = refl
-canPullOutSuccZ' a (positive zero (le x ())) c
-canPullOutSuccZ' a (positive (succ b) _) (negative zero (le x ()))
-canPullOutSuccZ' a (positive (succ b) y) (negative (succ c) x) with positive (succ b) y +Z' negative (succ c) x
-canPullOutSuccZ' a (positive (succ b) y) (negative (succ c) x) | negative zero (le x₁ ())
-canPullOutSuccZ' a (positive (succ b) y) (negative (succ c) x) | negative (succ sum) pr = refl
-canPullOutSuccZ' a (positive (succ b) y) (negative (succ c) x) | positive zero (le x₁ ())
-canPullOutSuccZ' a (positive (succ b) y) (negative (succ c) x) | positive (succ sum) pr = refl
-canPullOutSuccZ' a (positive (succ b) y) (negative (succ c) x) | zZero = refl
-canPullOutSuccZ' a (positive (succ b) _) (positive zero (le x ()))
-canPullOutSuccZ' a (positive (succ b) _) (positive (succ c) x) = refl
-canPullOutSuccZ' a (positive (succ b) _) zZero = refl
-canPullOutSuccZ' a zZero (negative zero (le x ()))
-canPullOutSuccZ' a zZero (negative (succ c) x) = refl
-canPullOutSuccZ' a zZero (positive zero (le x ()))
-canPullOutSuccZ' a zZero (positive (succ c) x) = refl
-canPullOutSuccZ' a zZero zZero = refl
-
-canPullOutSuccZ : (a : ℕ) → (b : ℤSimple) → (positive (succ (succ a)) (succIsPositive (succ a))) *Z' b ≡ b +Z' (positive (succ a) (succIsPositive a)) *Z' b
-canPullOutSuccZ a b = ans b
-  where
-    ans : (b : ℤSimple) → (positive (succ (succ a)) (succIsPositive (succ a))) *Z' b ≡ b +Z' (positive (succ a) (succIsPositive a)) *Z' b
-    ans (negative zero (le x ()))
-    ans (negative (succ b) x) = refl
-    ans (positive zero (le x ()))
-    ans (positive (succ b) x) = refl
-    ans zZero = refl
-
-
-swapAdds : (a c : ℕ) → (a +N succ c) +N succ (a +N succ c) ≡ (a +N succ a) +N succ (c +N succ c)
-swapAdds a c rewrite additionNIsAssociative a (succ c) (succ (a +N succ c)) | additionNIsAssociative a (succ a) (succ (c +N succ c)) = applyEquality (λ t → a +N succ t) help'
-  where
-    help' : c +N succ (a +N succ c) ≡ a +N succ (c +N succ c)
-    help' rewrite Semiring.commutative ℕSemiring c (succ (a +N succ c)) | Semiring.commutative ℕSemiring (a +N succ c) c | Semiring.commutative ℕSemiring (succ c) (a +N succ c) | additionNIsAssociative a (succ c) (succ c) = refl
-
-lemmaDistributive : (a : ℕ) → (b c : ℤSimple) → (positive (succ a) (succIsPositive a)) *Z' (b +Z' c) ≡ positive (succ a) (succIsPositive a) *Z' b +Z' positive (succ a) (succIsPositive a) *Z' c
-lemmaDistributive zero (negative zero (le x ())) c
-lemmaDistributive zero (negative (succ b) prB) (negative zero (le x ()))
-lemmaDistributive zero (negative (succ b) prB) (negative (succ a) x) rewrite Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring b 0 | Semiring.commutative ℕSemiring (b +N succ a) 0 = refl
-
-lemmaDistributive zero (negative (succ b) prB) (positive zero (le x ()))
-lemmaDistributive zero (negative (succ b) prB) (positive (succ a) x) rewrite oneIsIdentity' (negative (succ b) prB +Z' positive (succ a) x) | Semiring.commutative ℕSemiring b 0 | Semiring.commutative ℕSemiring a 0 | <NRefl x (logical<NImpliesLe (record {})) | <NRefl prB (logical<NImpliesLe (record {})) = refl
-lemmaDistributive zero (negative (succ b) prB) zZero = refl
-lemmaDistributive zero (positive zero (le x ())) c
-lemmaDistributive zero (positive (succ b) prB) (negative zero (le x ()))
-lemmaDistributive zero (positive (succ b) prB) (negative (succ a) x) rewrite Semiring.commutative ℕSemiring b 0 | Semiring.commutative ℕSemiring a 0 | oneIsIdentity' (positive (succ b) prB +Z' negative (succ a) x) | <NRefl prB (logical<NImpliesLe (record {})) | <NRefl x (logical<NImpliesLe (record {})) = refl
-lemmaDistributive zero (positive (succ b) prB) (positive zero (le x ()))
-lemmaDistributive zero (positive (succ b) prB) (positive (succ a) x) rewrite Semiring.commutative ℕSemiring b 0 | Semiring.commutative ℕSemiring a 0 = help2 ((b +N succ a) +N 0) (b +N succ a) (applyEquality succ lem)
-  where
-    help2 : (a b : ℕ) → (pr : succ a ≡ succ b) → positive (succ a) (succIsPositive _) ≡ positive (succ b) (succIsPositive _)
-    help2 a .a refl = refl
-    lem : (b +N succ a) +N 0 ≡ b +N succ a
-    lem rewrite Semiring.commutative ℕSemiring (b +N succ a) 0 = refl
-lemmaDistributive zero (positive (succ b) prB) zZero = refl
-lemmaDistributive zero zZero c rewrite oneIsIdentity' (zZero +Z' c) | oneIsIdentity' c = refl
-lemmaDistributive (succ a) b c = lemmV''
-  where
-    internallemma' : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ (b +Z' c) +Z' (positive (succ a) (succIsPositive a)) *Z' (b +Z' c)
-    internallemma' = canPullOutSuccZ' a b c
-    p : positive (succ (succ a)) (succIsPositive (succ a)) *Z' b ≡ b +Z' positive (succ a) (succIsPositive a) *Z' b
-    p = canPullOutSuccZ a b
-    q : positive (succ (succ a)) (succIsPositive (succ a)) *Z' c ≡ c +Z' positive (succ a) (succIsPositive a) *Z' c
-    q = canPullOutSuccZ a c
-    indHyp : (positive (succ a) (succIsPositive a)) *Z' (b +Z' c) ≡ positive (succ a) (succIsPositive a) *Z' b +Z' positive (succ a) (succIsPositive a) *Z' c
-    indHyp = lemmaDistributive a b c
-    lemm : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ (b +Z' c) +Z' (positive (succ a) (succIsPositive a) *Z' b +Z' positive (succ a) (succIsPositive a) *Z' c)
-    lemm rewrite equalityCommutative indHyp = internallemma'
-    lemm' : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ b +Z' (c +Z' ((positive (succ a) (succIsPositive a) *Z' b +Z' positive (succ a) (succIsPositive a) *Z' c)))
-    lemm' rewrite additionZ'IsAssociative b c (positive (succ a) (succIsPositive a) *Z' b +Z' positive (succ a) (succIsPositive a) *Z' c) = lemm
-    lemm'' : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ b +Z' (((positive (succ a) (succIsPositive a) *Z' b +Z' positive (succ a) (succIsPositive a) *Z' c)) +Z' c)
-    inter : ((positive (succ a) (succIsPositive a) *Z' b +Z' positive (succ a) (succIsPositive a) *Z' c)) +Z' c ≡ positive (succ a) (succIsPositive a) *Z' b +Z' ((positive (succ a) (succIsPositive a) *Z' c) +Z' c)
-    lemm''' : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ b +Z' (positive (succ a) (succIsPositive a) *Z' b +Z' ((positive (succ a) (succIsPositive a) *Z' c) +Z' c))
-    lemm'''' : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ (b +Z' (positive (succ a) (succIsPositive a) *Z' b)) +Z' ((positive (succ a) (succIsPositive a) *Z' c) +Z' c)
-    lemm'''' rewrite equalityCommutative (additionZ'IsAssociative b (positive (succ a) (succIsPositive a) *Z' b) ((positive (succ a) (succIsPositive a) *Z' c) +Z' c)) = lemm'''
-    lemmV : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ (positive (succ (succ a)) (succIsPositive (succ a)) *Z' b) +Z' ((positive (succ a) (succIsPositive a) *Z' c) +Z' c)
-    lemmV rewrite p = lemm''''
-    lemmV' : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ (positive (succ (succ a)) (succIsPositive (succ a)) *Z' b) +Z' (c +Z' (positive (succ a) (succIsPositive a) *Z' c))
-    lemmV' rewrite additionZ'IsCommutative c (positive (succ a) (succIsPositive a) *Z' c) = lemmV
-    lemmV'' : (positive (succ (succ a)) (succIsPositive (succ a))) *Z' (b +Z' c) ≡ (positive (succ (succ a)) (succIsPositive (succ a)) *Z' b) +Z' (positive (succ (succ a)) (succIsPositive (succ a)) *Z' c)
-    lemmV'' rewrite q = lemmV'
-    lemm'' rewrite additionZ'IsCommutative ((positive (succ a) (succIsPositive a) *Z' b +Z' positive (succ a) (succIsPositive a) *Z' c)) c = lemm'
-    inter = equalityCommutative (additionZ'IsAssociative (positive (succ a) (succIsPositive a) *Z' b) (positive (succ a) (succIsPositive a) *Z' c) c)
-    lemm''' rewrite equalityCommutative inter = lemm''
-
-addIsZero : (a b : ℕ) → {pr1 : 0 <N a} → {pr2 : 0 <N b} → ((positive a pr1) +Z' (negative b pr2) ≡ zZero) → a ≡ b
-addIsZero zero b {le x ()} {pr2} pr
-addIsZero (succ a) zero {pr1} {le x ()} pr
-addIsZero (succ zero) (succ zero) {pr1} {pr2} pr = refl
-addIsZero (succ zero) (succ (succ b)) {pr1} {pr2} pr = exFalso (f pr)
-  where
-    f : (negative (succ b) (logical<NImpliesLe (record {})) ≡ zZero) → False
-    f ()
-addIsZero (succ (succ a)) (succ zero) {pr1} {pr2} pr = exFalso (f pr)
-  where
-    f : (positive (succ a) (logical<NImpliesLe (record {})) ≡ zZero) → False
-    f ()
-addIsZero (succ (succ a)) (succ (succ b)) {pr1} {pr2} pr = applyEquality succ (addIsZero (succ a) (succ b) {succIsPositive a} {succIsPositive b} p)
-  where
-    q : positive (succ (succ a)) pr1 +Z' negative (succ (succ b)) pr2 ≡ positive (succ a) (succIsPositive a) +Z' negative (succ b) (succIsPositive b)
-    q = canKnockOneOff+Z' (succ a) (succ b) {succIsPositive a} {succIsPositive b} {pr1} {pr2}
-    p : positive (succ a) (succIsPositive a) +Z' negative (succ b) (succIsPositive b) ≡ zZero
-    p rewrite equalityCommutative q = pr
-
-addIsZero' : (a : ℕ) → (negative (succ a) (succIsPositive a)) +Z' (positive (succ a) (succIsPositive a)) ≡ zZero
-addIsZero' (zero) = refl
-addIsZero' (succ a) = transitivity q p
-  where
-    p : negative (succ a) (succIsPositive a) +Z' positive (succ a) (succIsPositive a) ≡ zZero
-    p = addIsZero' a
-    q : negative (succ (succ a)) (succIsPositive (succ a)) +Z' positive (succ (succ a)) (succIsPositive (succ a)) ≡ negative (succ a) (succIsPositive a) +Z' positive (succ a) (succIsPositive a)
-    q = canKnockOneOff+Z'2 (succ a) (succ a) {succIsPositive a} {succIsPositive a} {succIsPositive (succ a)} {succIsPositive (succ a)}
-
-timesNegPosPos : (a b c : ℕ) → (negative (succ a) (succIsPositive a)) *Z' ((positive (succ b) (succIsPositive b)) +Z' (positive (succ c) (succIsPositive c))) ≡ (positive (succ a) (succIsPositive a)) *Z' ((negative (succ b) (succIsPositive b)) +Z' (negative (succ c) (succIsPositive c)))
-timesNegPosPos a b c = refl
-
-diffProof : (a b : ℕ) → (sum1 sum2 : ℕ) → (pr1 : succ a +N succ b ≡ sum1) → (pr2 : succ a +N succ b ≡ sum2) → (prSums : sum1 ≡ sum2) → plusZ' sum1 (negative (succ a) (succIsPositive a)) (positive (succ b) (succIsPositive b)) pr1 ≡ plusZ' sum2 (negative (succ a) (succIsPositive a)) (positive (succ b) (succIsPositive b)) pr2
-diffProof a b .(succ (a +N succ b)) .(succ (a +N succ b)) refl refl refl = refl
-
-diffProof' : (a b : ℕ) → (sum1 sum2 : ℕ) → (pr1 : succ a +N succ b ≡ sum1) → (pr2 : succ a +N succ b ≡ sum2) → (prSums : sum1 ≡ sum2) → plusZ' sum1 (positive (succ a) (succIsPositive a)) (negative (succ b) (succIsPositive b)) pr1 ≡ plusZ' sum2 (positive (succ a) (succIsPositive a)) (negative (succ b) (succIsPositive b)) pr2
-diffProof' a b .(succ (a +N succ b)) .(succ (a +N succ b)) refl refl refl = refl
-
-timesNegPosNeg : (a b c : ℕ) → (negative (succ a) (succIsPositive a)) *Z' ((positive (succ b) (succIsPositive b)) +Z' (negative (succ c) (succIsPositive c))) ≡ (positive (succ a) (succIsPositive a)) *Z' ((negative (succ b) (succIsPositive b)) +Z' (positive (succ c) (succIsPositive c)))
-timesNegPosNeg zero zero zero = refl
-timesNegPosNeg zero zero (succ c) = refl
-timesNegPosNeg zero (succ b) zero = refl
-timesNegPosNeg zero (succ b) (succ c) = identityOfIndiscernablesRight _ _ _ _≡_ ans'' (applyEquality (λ t → positive 1 _ *Z' t) (knocked'))
-  where
-    knocked : positive (succ (succ b)) (succIsPositive (succ b)) +Z' negative (succ (succ c)) (succIsPositive (succ c)) ≡ positive (succ b) _ +Z' negative (succ c) _
-    knocked = canKnockOneOff+Z' (succ b) (succ c) {succIsPositive b} {succIsPositive c} {succIsPositive (succ b)} {succIsPositive (succ c)}
-    knocked' : negative (succ b) (succIsPositive b) +Z' positive (succ c) (succIsPositive c) ≡ negative (succ (succ b)) (succIsPositive (succ b)) +Z' positive (succ (succ c)) (succIsPositive (succ c))
-    knocked' rewrite additionZ'IsCommutative (negative (succ b) (succIsPositive b)) (positive (succ c) (succIsPositive c)) | additionZ'IsCommutative (negative (succ (succ b)) (succIsPositive (succ b))) (positive (succ (succ c)) (succIsPositive (succ c))) = diffProof' c b (succ (c +N succ b)) (c +N succ (succ b)) refl help (equalityCommutative (succExtracts c (succ b)))
-      where
-        help : (succ (c +N succ b)) ≡ c +N succ (succ b)
-        help = _
-    ans : negative 1 (succIsPositive zero) *Z' (positive (succ b) _ +Z' negative (succ c) _) ≡ positive 1 _ *Z' (negative (succ b) _ +Z' positive (succ c) _)
-    ans = timesNegPosNeg zero b c
-    ans' : negative 1 _ *Z' (positive (succ (succ b)) (succIsPositive (succ b)) +Z' negative (succ (succ c)) (succIsPositive (succ c))) ≡ negative 1 _ *Z' (positive (succ b) _ +Z' negative (succ c) _)
-    ans' = applyEquality (λ t → negative 1 _ *Z' t) knocked
-    ans'' : negative 1 _ *Z' (positive (succ (succ b)) (succIsPositive (succ b)) +Z' negative (succ (succ c)) (succIsPositive (succ c))) ≡ positive 1 _ *Z' (negative (succ b) _ +Z' positive (succ c) _)
-    ans'' = identityOfIndiscernablesRight _ _ _ _≡_ ans' ans
-timesNegPosNeg (succ a) zero zero = refl
-timesNegPosNeg (succ a) zero (succ c) = refl
-timesNegPosNeg (succ a) (succ b) zero = refl
-timesNegPosNeg (succ a) (succ b) (succ c) = identityOfIndiscernablesRight _ _ _ _≡_ ans'' (applyEquality (λ t → positive (succ (succ a)) (succIsPositive (succ a)) *Z' t) (knocked'))
-  where
-    knocked : positive (succ (succ b)) (succIsPositive (succ b)) +Z' negative (succ (succ c)) (succIsPositive (succ c)) ≡ positive (succ b) _ +Z' negative (succ c) _
-    knocked = canKnockOneOff+Z' (succ b) (succ c) {succIsPositive b} {succIsPositive c} {succIsPositive (succ b)} {succIsPositive (succ c)}
-    knocked' : negative (succ b) (succIsPositive b) +Z' positive (succ c) (succIsPositive c) ≡ negative (succ (succ b)) (succIsPositive (succ b)) +Z' positive (succ (succ c)) (succIsPositive (succ c))
-    knocked' rewrite additionZ'IsCommutative (negative (succ b) (succIsPositive b)) (positive (succ c) (succIsPositive c)) | additionZ'IsCommutative (negative (succ (succ b)) (succIsPositive (succ b))) (positive (succ (succ c)) (succIsPositive (succ c))) = diffProof' c b (succ (c +N succ b)) (c +N succ (succ b)) refl help (equalityCommutative (succExtracts c (succ b)))
-      where
-        help : (succ (c +N succ b)) ≡ c +N succ (succ b)
-        help = _
-    ans : negative (succ (succ a)) (succIsPositive (succ a)) *Z' (positive (succ b) _ +Z' negative (succ c) _) ≡ positive (succ (succ a)) (succIsPositive (succ a)) *Z' (negative (succ b) _ +Z' positive (succ c) _)
-    ans = timesNegPosNeg (succ a) b c
-    ans' : negative (succ (succ a)) (succIsPositive (succ a)) *Z' (positive (succ (succ b)) (succIsPositive (succ b)) +Z' negative (succ (succ c)) (succIsPositive (succ c))) ≡ negative (succ (succ a)) (succIsPositive (succ a)) *Z' (positive (succ b) _ +Z' negative (succ c) _)
-    ans' = applyEquality (λ t → negative (succ (succ a)) (succIsPositive (succ a)) *Z' t) knocked
-    ans'' : negative (succ (succ a)) (succIsPositive (succ a)) *Z' (positive (succ (succ b)) (succIsPositive (succ b)) +Z' negative (succ (succ c)) (succIsPositive (succ c))) ≡ positive (succ (succ a)) (succIsPositive (succ a)) *Z' (negative (succ b) _ +Z' positive (succ c) _)
-    ans'' = identityOfIndiscernablesRight _ _ _ _≡_ ans' ans
-
-timesNegNegPos : (a b c : ℕ) → (negative (succ a) (succIsPositive a)) *Z' ((negative (succ b) (succIsPositive b)) +Z' (positive (succ c) (succIsPositive c))) ≡ (positive (succ a) (succIsPositive a)) *Z' ((positive (succ b) (succIsPositive b)) +Z' (negative (succ c) (succIsPositive c)))
-timesNegNegPos a b c rewrite additionZ'IsCommutative (negative (succ b) (succIsPositive b)) (positive (succ c) (succIsPositive c)) | additionZ'IsCommutative (positive (succ b) (succIsPositive b)) (negative (succ c) (succIsPositive c)) = timesNegPosNeg a c b
-
-additionZ'DistributiveMulZ' : (a b c : ℤSimple) → (a *Z' (b +Z' c)) ≡ (a *Z' b +Z' a *Z' c)
-additionZ'DistributiveMulZ' (negative zero (le x ())) b c
-additionZ'DistributiveMulZ' (negative (succ a) x) (negative zero (le y ())) (negative c prC)
-additionZ'DistributiveMulZ' (negative (succ a) x) (negative (succ b) prB) (negative zero (le y ()))
-additionZ'DistributiveMulZ' (negative (succ a) x) (negative (succ b) prB) (negative (succ c) prC) = lemmaDistributive a (positive (succ b) prB) (positive (succ c) prC)
-additionZ'DistributiveMulZ' (negative (succ a) x) (negative zero (le y ())) (positive c prC)
-additionZ'DistributiveMulZ' (negative (succ a) x) (negative (succ b) prB) (positive zero (le y ()))
-additionZ'DistributiveMulZ' (negative (succ a) x) (negative (succ b) prB) (positive (succ c) prC) rewrite <NRefl x (succIsPositive a) | <NRefl prB (succIsPositive b) | <NRefl prC (succIsPositive c) = help
-  where
-    inter : (negative (succ a) (succIsPositive a)) *Z' ((negative (succ b) (succIsPositive b)) +Z' (positive (succ c) (succIsPositive c))) ≡ positive (succ a) (succIsPositive a) *Z' (positive (succ b) (succIsPositive b) +Z' negative (succ c) (succIsPositive c))
-    inter = timesNegNegPos a b c
-    lhs : positive (succ a) (succIsPositive a) *Z' (positive (succ b) (succIsPositive b) +Z' negative (succ c) (succIsPositive c)) ≡ positive (succ a) (succIsPositive a) *Z' positive (succ b) (succIsPositive b) +Z' (negative (succ a) (succIsPositive a) *Z' positive (succ c) (succIsPositive c))
-    lhs = lemmaDistributive a (positive (succ b) (succIsPositive b)) (negative (succ c) (succIsPositive c))
-    help : (negative (succ a) (succIsPositive a)) *Z' ((negative (succ b) (succIsPositive b)) +Z' (positive (succ c) (succIsPositive c))) ≡ negative (succ a) (succIsPositive a) *Z' negative (succ b) (succIsPositive b) +Z' (negative (succ a) (succIsPositive a) *Z' positive (succ c) (succIsPositive c))
-    help = transitivity inter lhs
-additionZ'DistributiveMulZ' (negative (succ a) x) (negative zero (le y ())) zZero
-additionZ'DistributiveMulZ' (negative (succ a) x) (negative (succ b) prB) zZero = refl
-additionZ'DistributiveMulZ' (negative (succ a) x) (positive b prB) (negative zero (le y ()))
-additionZ'DistributiveMulZ' (negative (succ a) x) (positive zero (le y ())) (negative (succ c) prC)
-additionZ'DistributiveMulZ' (negative (succ a) x) (positive (succ b) prB) (negative (succ c) prC) rewrite <NRefl x (succIsPositive a) | <NRefl prB (succIsPositive b) | <NRefl prC (succIsPositive c) = help
-  where
-    inter : (negative (succ a) (succIsPositive a)) *Z' ((positive (succ b) (succIsPositive b)) +Z' (negative (succ c) (succIsPositive c))) ≡ positive (succ a) (succIsPositive a) *Z' (negative (succ b) (succIsPositive b) +Z' positive (succ c) (succIsPositive c))
-    inter = timesNegPosNeg a b c
-    lhs : positive (succ a) (succIsPositive a) *Z' (negative (succ b) (succIsPositive b) +Z' positive (succ c) (succIsPositive c)) ≡ positive (succ a) (succIsPositive a) *Z' negative (succ b) (succIsPositive b) +Z' (positive (succ a) (succIsPositive a) *Z' positive (succ c) (succIsPositive c))
-    lhs = lemmaDistributive a (negative (succ b) (succIsPositive b)) (positive (succ c) (succIsPositive c))
-    help : (negative (succ a) (succIsPositive a)) *Z' ((positive (succ b) (succIsPositive b)) +Z' (negative (succ c) (succIsPositive c))) ≡ negative (succ a) (succIsPositive a) *Z' positive (succ b) (succIsPositive b) +Z' (negative (succ a) (succIsPositive a) *Z' negative (succ c) (succIsPositive c))
-    help = transitivity inter lhs
-additionZ'DistributiveMulZ' (negative (succ a) x) (positive b prB) (positive zero (le y ()))
-additionZ'DistributiveMulZ' (negative (succ a) x) (positive 0 (le y ())) (positive (succ c) prC)
-additionZ'DistributiveMulZ' (negative (succ a) x) (positive (succ b) prB) (positive (succ c) prC) rewrite timesNegPosPos a b c = applyEquality (λ t → negative (succ t) (succIsPositive t)) help
-    where
-      help : (b +N succ c) +N a *N succ (b +N succ c) ≡ (b +N a *N succ b) +N succ (c +N a *N succ c)
-      help rewrite Semiring.+DistributesOver* ℕSemiring a (succ b) (succ c) | Semiring.+Associative ℕSemiring (b +N succ c) (a *N succ b) (a *N succ c) | additionNIsAssociative b (succ c) (a *N succ b) | Semiring.commutative ℕSemiring (succ c) (a *N succ b) | equalityCommutative (additionNIsAssociative b (a *N succ b) (succ c)) | additionNIsAssociative (b +N a *N succ b) (succ c) (a *N succ c) = refl
-additionZ'DistributiveMulZ' (negative (succ a) x) (positive zero (le y ())) zZero
-additionZ'DistributiveMulZ' (negative (succ a) x) (positive (succ b) prB) zZero = refl
-additionZ'DistributiveMulZ' (negative (succ a) x) zZero (negative zero (le y ()))
-additionZ'DistributiveMulZ' (negative (succ a) x) zZero (negative (succ c) prC) = refl
-additionZ'DistributiveMulZ' (negative (succ a) x) zZero (positive zero (le y ()))
-additionZ'DistributiveMulZ' (negative (succ a) x) zZero (positive (succ c) prC) = refl
-additionZ'DistributiveMulZ' (negative (succ a) x) zZero zZero = refl
-additionZ'DistributiveMulZ' (positive zero (le x ())) b c
-additionZ'DistributiveMulZ' (positive (succ a) x) b c rewrite <NRefl x (succIsPositive a) = lemmaDistributive a b c
-additionZ'DistributiveMulZ' zZero b c = refl
-
-additionZDistributiveMulZ : (a b c : ℤ) → (a *Z (b +Z c)) ≡ (a *Z b) +Z (a *Z c)
-additionZDistributiveMulZ a b c = identityOfIndiscernablesRight _ _ _ _≡_ lem12 (applyEquality (λ t → a *Z b +Z (a *Z t)) (zIsZ c))
-  where
-    lem1 : convertZ' ((convertZ a) *Z' ((convertZ b) +Z' (convertZ c))) ≡ convertZ' ((convertZ a *Z' convertZ b) +Z' (convertZ a *Z' convertZ c))
-    lem2 : convertZ' (convertZ a) *Z convertZ' ((convertZ b) +Z' (convertZ c)) ≡ convertZ' ((convertZ a *Z' convertZ b) +Z' (convertZ a *Z' convertZ c))
-    lem3 : a *Z convertZ' ((convertZ b) +Z' (convertZ c)) ≡ convertZ' ((convertZ a *Z' convertZ b) +Z' (convertZ a *Z' convertZ c))
-    lem4 : a *Z (convertZ' (convertZ b) +Z convertZ' (convertZ c)) ≡ convertZ' ((convertZ a *Z' convertZ b) +Z' (convertZ a *Z' convertZ c))
-    lem5 : a *Z (b +Z convertZ' (convertZ c)) ≡ convertZ' ((convertZ a *Z' convertZ b) +Z' (convertZ a *Z' convertZ c))
-    lem6 : a *Z (b +Z c) ≡ convertZ' ((convertZ a *Z' convertZ b) +Z' (convertZ a *Z' convertZ c))
-    lem7 : a *Z (b +Z c) ≡ convertZ' (convertZ a *Z' convertZ b) +Z convertZ' (convertZ a *Z' convertZ c)
-    lem8 : a *Z (b +Z c) ≡ (convertZ' (convertZ a) *Z (convertZ' (convertZ b))) +Z convertZ' (convertZ a *Z' convertZ c)
-    lem9 : a *Z (b +Z c) ≡ (a *Z (convertZ' (convertZ b))) +Z convertZ' (convertZ a *Z' convertZ c)
-    lem10 : a *Z (b +Z c) ≡ (a *Z b) +Z convertZ' (convertZ a *Z' convertZ c)
-    lem11 : a *Z (b +Z c) ≡ (a *Z b) +Z (convertZ' (convertZ a) *Z convertZ' (convertZ c))
-    lem12 : a *Z (b +Z c) ≡ (a *Z b) +Z (a *Z convertZ' (convertZ c))
-    lem12 = identityOfIndiscernablesRight _ _ _ _≡_ lem11 (applyEquality (λ t → a *Z b +Z (t *Z convertZ' (convertZ c))) (zIsZ a))
-    lem11 = identityOfIndiscernablesRight _ _ _ _≡_ lem10 (applyEquality (λ t → a *Z b +Z t) (convertZ'DistributesOver*Z (convertZ a) _))
-    lem10 = identityOfIndiscernablesRight _ _ _ _≡_ lem9 (applyEquality (λ t → a *Z t +Z convertZ' (convertZ a *Z' convertZ c)) (zIsZ b))
-    lem9 = identityOfIndiscernablesRight _ _ _ _≡_ lem8 (applyEquality (λ t → t *Z (convertZ' (convertZ b)) +Z convertZ' (convertZ a *Z' convertZ c)) (zIsZ a))
-    lem8 = identityOfIndiscernablesRight _ _ _ _≡_ lem7 (applyEquality (λ t → t +Z convertZ' (convertZ a *Z' convertZ c)) (convertZ'DistributesOver*Z (convertZ a) _))
-    lem7 = identityOfIndiscernablesRight _ _ _ _≡_ lem6 (plusIsPlus (convertZ a *Z' convertZ b) _)
-    lem6 = identityOfIndiscernablesLeft _ _ _ _≡_ lem5 (applyEquality (λ t → a *Z (b +Z t)) (zIsZ c))
-    lem5 = identityOfIndiscernablesLeft _ _ _ _≡_ lem4 (applyEquality (λ t → a *Z (t +Z convertZ' (convertZ c))) (zIsZ b))
-    lem4 = identityOfIndiscernablesLeft _ _ _ _≡_ lem3 (applyEquality (λ t → a *Z t) (plusIsPlus (convertZ b) _))
-    lem3 = identityOfIndiscernablesLeft _ _ _ _≡_ lem2 (applyEquality (λ t → t *Z (convertZ' ((convertZ b) +Z' convertZ c))) (zIsZ a))
-    lem2 = identityOfIndiscernablesLeft _ _ _ _≡_ lem1 (convertZ'DistributesOver*Z (convertZ a) _)
-    lem1 = applyEquality convertZ' (additionZ'DistributiveMulZ' (convertZ a) (convertZ b) (convertZ c))
-
-additionZRespectsOrder : (a b c : ℤ) → (a <Z b) → (a +Z c <Z b +Z c)
-additionZRespectsOrder a b c (le x proof) = le x (identityOfIndiscernablesLeft ((nonneg (succ x) +Z a) +Z c) (b +Z c) (nonneg (succ x) +Z (a +Z c)) _≡_ (applyEquality (λ t → t +Z c) proof) (equalityCommutative (additionZIsAssociative (nonneg (succ x)) a c)))
-
-nonnegNotLessNegsucc : (a b : ℕ) → (nonneg a <Z negSucc b) → False
-nonnegNotLessNegsucc a b (le x proof) = nonnegIsNotNegsucc proof
-
-productOfPositivesIsPositive : (a b : ℤ) → (nonneg zero <Z a) → (nonneg zero <Z b) → (nonneg 0 <Z a *Z b)
-productOfPositivesIsPositive (nonneg zero) (nonneg b) pr1 pr2 = exFalso (lessZIrreflexive {nonneg 0} pr1)
-productOfPositivesIsPositive (nonneg (succ a)) (nonneg zero) pr1 pr2 = exFalso (lessZIrreflexive {nonneg 0} pr2)
-productOfPositivesIsPositive (nonneg (succ a)) (nonneg (succ b)) pr1 pr2 rewrite multiplyingNonnegIsHom (succ a) (succ b) = lessIsPreservedNToZ (succIsPositive (b +N a *N succ b))
-productOfPositivesIsPositive (nonneg zero) (negSucc b) pr1 pr2 = exFalso (nonnegNotLessNegsucc 0 b pr2)
-productOfPositivesIsPositive (nonneg (succ a)) (negSucc b) pr1 pr2 = exFalso (nonnegNotLessNegsucc 0 b pr2)
-productOfPositivesIsPositive (negSucc x) b pr1 pr2 = exFalso (nonnegNotLessNegsucc 0 x pr1)
-
-lessZTransitive : {a b c : ℤ} → (a <Z b) → (b <Z c) → (a <Z c)
-lessZTransitive {a} {b} {c} (le d1 pr1) (le d2 pr2) rewrite equalityCommutative pr1 = le (d1 +N succ d2) pr
-  where
-    pr : nonneg (succ (d1 +N succ d2)) +Z a ≡ c
-    pr rewrite additionZIsAssociative (nonneg (succ d2)) (nonneg (succ d1)) a | Semiring.commutative ℕSemiring (succ d2) (succ d1) = pr2
-
-ℤGroup : Group (reflSetoid ℤ) (_+Z_)
-Group.wellDefined ℤGroup {a} {b} {.a} {.b} refl refl = refl
-Group.identity ℤGroup = nonneg zero
-Group.inverse ℤGroup = additiveInverseZ
-Group.multAssoc ℤGroup {a} {b} {c} = additionZIsAssociative a b c
-Group.multIdentLeft ℤGroup {a} = refl
-Group.multIdentRight ℤGroup {a} = zeroIsAdditiveIdentityRightZ a
-Group.invLeft ℤGroup {a} = addInverseLeftZ a
-Group.invRight ℤGroup {a} = addInverseRightZ a
-
-ℤAbGrp : AbelianGroup ℤGroup
-ℤAbGrp = record { commutative = λ {a} {b} → additionZIsCommutative a b }
-
-ℤRing : Ring (reflSetoid ℤ) (_+Z_) (_*Z_)
-Ring.additiveGroup ℤRing = ℤGroup
-Ring.multWellDefined ℤRing {r} {s} {.r} {.s} refl refl = refl
-Ring.1R ℤRing = nonneg (succ zero)
-Ring.groupIsAbelian ℤRing {a} {b} = additionZIsCommutative a b
-Ring.multAssoc ℤRing {a} {b} {c} = multiplicationZIsAssociative a b c
-Ring.multCommutative ℤRing {a} {b} = multiplicationZIsCommutative a b
-Ring.multDistributes ℤRing {a} {b} {c} = additionZDistributiveMulZ a b c
-Ring.multIdentIsIdent ℤRing {a} = multiplicativeIdentityOneZLeft a
-
-negsuccTimesNonneg : {a b : ℕ} → (negSucc a *Z nonneg (succ b)) ≡ nonneg 0 → False
-negsuccTimesNonneg {a} {b} pr with convertZ (negSucc a)
-negsuccTimesNonneg {a} {b} () | negative a₁ x
-negsuccTimesNonneg {a} {b} () | positive a₁ x
-negsuccTimesNonneg {a} {b} () | zZero
-
-negsuccTimesNegsucc : {a b : ℕ} → (negSucc a *Z negSucc b) ≡ nonneg 0 → False
-negsuccTimesNegsucc {a} {b} pr with convertZ (negSucc a)
-negsuccTimesNegsucc {a} {b} () | negative a₁ x
-negsuccTimesNegsucc {a} {b} () | positive a₁ x
-negsuccTimesNegsucc {a} {b} () | zZero
-
-ℤIntDom : IntegralDomain ℤRing
-IntegralDomain.intDom ℤIntDom {nonneg zero} {nonneg b} pr = inl refl
-IntegralDomain.intDom ℤIntDom {nonneg (succ a)} {nonneg zero} pr = inr refl
-IntegralDomain.intDom ℤIntDom {nonneg (succ a)} {nonneg (succ b)} pr = exFalso (naughtE (nonnegInjective (equalityCommutative (transitivity (equalityCommutative (multiplyingNonnegIsHom (succ a) (succ b))) pr))))
-IntegralDomain.intDom ℤIntDom {nonneg zero} {negSucc b} pr = inl refl
-IntegralDomain.intDom ℤIntDom {nonneg (succ a)} {negSucc b} pr = exFalso (negsuccTimesNonneg {b} {a} (transitivity (multiplicationZIsCommutative (negSucc b) (nonneg (succ a))) pr))
-IntegralDomain.intDom ℤIntDom {negSucc a} {nonneg zero} pr = inr refl
-IntegralDomain.intDom ℤIntDom {negSucc a} {nonneg (succ b)} pr = exFalso (negsuccTimesNonneg {a} {b} pr)
-IntegralDomain.intDom ℤIntDom {negSucc a} {negSucc b} pr = exFalso (negsuccTimesNegsucc {a} {b} pr)
-IntegralDomain.nontrivial ℤIntDom = λ ()
-
-ℤOrder : TotalOrder ℤ
-PartialOrder._<_ (TotalOrder.order ℤOrder) = _<Z_
-TotalOrder.totality ℤOrder a b = lessThanTotalZ {a} {b}
-PartialOrder.irreflexive (TotalOrder.order ℤOrder) = lessZIrreflexive
-PartialOrder.transitive (TotalOrder.order ℤOrder) {a} {b} {c} = lessZTransitive
-
-ℤOrderedRing : OrderedRing ℤRing (totalOrderToSetoidTotalOrder ℤOrder)
-OrderedRing.orderRespectsAddition ℤOrderedRing {a} {b} a<b c = additionZRespectsOrder a b c a<b
-OrderedRing.orderRespectsMultiplication ℤOrderedRing {a} {b} a<b = productOfPositivesIsPositive a b a<b
-
-_-Z_ : ℤ → ℤ → ℤ
-a -Z b = a +Z (additiveInverseZ b)
diff --git a/Numbers/Integers/Addition.agda b/Numbers/Integers/Addition.agda
new file mode 100644
index 0000000..a19c7a4
--- /dev/null
+++ b/Numbers/Integers/Addition.agda
@@ -0,0 +1,95 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Numbers.Naturals.Naturals
+open import Numbers.Integers.Definition
+open import Semirings.Definition
+open import Groups.Groups
+open import Groups.Definition
+open import Setoids.Setoids
+
+module Numbers.Integers.Addition where
+
+infix 15 _+Z_
+_+Z_ : ℤ → ℤ → ℤ
+nonneg zero +Z b = b
+nonneg (succ x) +Z nonneg y = nonneg (succ x +N y)
+nonneg (succ x) +Z negSucc zero = nonneg x
+nonneg (succ x) +Z negSucc (succ y) = nonneg x +Z negSucc y
+negSucc x +Z nonneg zero = negSucc x
+negSucc zero +Z nonneg (succ y) = nonneg y
+negSucc (succ x) +Z nonneg (succ y) = negSucc x +Z nonneg y
+negSucc x +Z negSucc y = negSucc (succ x +N y)
+
++Zinherits : (a b : ℕ) → nonneg (a +N b) ≡ (nonneg a) +Z (nonneg b)
++Zinherits zero b = refl
++Zinherits (succ a) b = refl
+
++ZCommutative : (a b : ℤ) → a +Z b ≡ b +Z a
++ZCommutative (nonneg zero) (nonneg zero) = refl
++ZCommutative (nonneg zero) (nonneg (succ y)) = applyEquality (λ i → nonneg (succ i)) (Semiring.commutative ℕSemiring 0 y)
++ZCommutative (nonneg (succ x)) (nonneg zero) = applyEquality (λ i → nonneg (succ i)) (Semiring.commutative ℕSemiring x 0)
++ZCommutative (nonneg (succ x)) (nonneg (succ y)) = applyEquality (λ i → nonneg (succ i)) (transitivity (Semiring.commutative ℕSemiring x (succ y)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring y x)) (Semiring.commutative ℕSemiring (succ x) y)))
++ZCommutative (nonneg zero) (negSucc y) = refl
++ZCommutative (nonneg (succ x)) (negSucc zero) = refl
++ZCommutative (nonneg (succ x)) (negSucc (succ y)) = +ZCommutative (nonneg x) (negSucc y)
++ZCommutative (negSucc x) (nonneg zero) = refl
++ZCommutative (negSucc zero) (nonneg (succ y)) = refl
++ZCommutative (negSucc (succ x)) (nonneg (succ y)) = +ZCommutative (negSucc x) (nonneg y)
++ZCommutative (negSucc x) (negSucc y) = applyEquality (λ i → negSucc (succ i)) (Semiring.commutative ℕSemiring x y)
+
++ZAssociative : (a b c : ℤ) → a +Z (b +Z c) ≡ (a +Z b) +Z c
++ZAssociative (nonneg zero) (nonneg b) (nonneg c) = refl
++ZAssociative (nonneg (succ a)) (nonneg zero) (nonneg c) rewrite Semiring.commutative ℕSemiring a 0 = refl
++ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg c) = applyEquality (λ i → nonneg (succ i)) (Semiring.+Associative ℕSemiring a (succ b) c)
++ZAssociative (nonneg zero) (nonneg b) (negSucc c) = refl
++ZAssociative (nonneg (succ a)) (nonneg zero) (negSucc c) rewrite Semiring.sumZeroRight ℕSemiring a = refl
++ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc zero) = applyEquality nonneg (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a b)) (Semiring.commutative ℕSemiring (succ b) a))
++ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc (succ c)) = transitivity (+ZAssociative (nonneg (succ a)) (nonneg b) (negSucc c)) (applyEquality (λ i → nonneg i +Z negSucc c) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a b)) (Semiring.commutative ℕSemiring (succ b) a)))
++ZAssociative (nonneg zero) (negSucc b) c = refl
++ZAssociative (nonneg (succ a)) (negSucc zero) (nonneg zero) = +ZCommutative (nonneg 0) (nonneg a)
++ZAssociative (nonneg (succ a)) (negSucc zero) (nonneg (succ c)) = transitivity (applyEquality nonneg (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a c)) (Semiring.commutative ℕSemiring (succ c) a))) (+Zinherits a (succ c))
++ZAssociative (nonneg (succ a)) (negSucc zero) (negSucc c) = refl
++ZAssociative (nonneg (succ a)) (negSucc (succ b)) (nonneg zero) = +ZCommutative (nonneg 0) _
++ZAssociative (nonneg (succ a)) (negSucc (succ b)) (nonneg (succ c)) = transitivity (applyEquality (nonneg (succ a) +Z_) (+ZCommutative (negSucc b) (nonneg c))) (transitivity (+ZAssociative (nonneg (succ a)) (nonneg c) (negSucc b)) (transitivity (transitivity (transitivity (transitivity (applyEquality (λ i → nonneg (succ i) +Z negSucc b) (Semiring.commutative ℕSemiring a c)) (+ZCommutative (nonneg (succ (c +N a))) (negSucc b))) (applyEquality (negSucc b +Z_) (+ZCommutative (nonneg (succ c)) (nonneg a)))) (+ZAssociative (negSucc b) (nonneg a) (nonneg (succ c)))) (applyEquality (_+Z nonneg (succ c)) (+ZCommutative (negSucc b) (nonneg a)))))
++ZAssociative (nonneg (succ a)) (negSucc (succ b)) (negSucc c) = +ZAssociative (nonneg a) (negSucc b) (negSucc c)
++ZAssociative (negSucc a) (nonneg zero) c = refl
++ZAssociative (negSucc zero) (nonneg (succ b)) (nonneg c) = +Zinherits b c
++ZAssociative (negSucc zero) (nonneg (succ b)) (negSucc zero) = +ZCommutative (negSucc 0) (nonneg b)
++ZAssociative (negSucc zero) (nonneg (succ b)) (negSucc (succ c)) = transitivity (+ZCommutative (negSucc 0) (nonneg b +Z negSucc c)) (transitivity (equalityCommutative (+ZAssociative (nonneg b) (negSucc c) (negSucc 0))) (applyEquality (λ i → nonneg b +Z negSucc (succ i)) (Semiring.sumZeroRight ℕSemiring c)))
++ZAssociative (negSucc (succ a)) (nonneg (succ b)) (nonneg zero) = transitivity (applyEquality (λ i → negSucc a +Z (nonneg i)) (Semiring.sumZeroRight ℕSemiring b)) (+ZCommutative (nonneg 0) (negSucc a +Z nonneg b))
++ZAssociative (negSucc (succ a)) (nonneg (succ b)) (nonneg (succ c)) = transitivity (applyEquality (negSucc a +Z_) (+Zinherits b (succ c))) (+ZAssociative (negSucc a) (nonneg b) (nonneg (succ c)))
++ZAssociative (negSucc (succ a)) (nonneg (succ b)) (negSucc zero) = transitivity (+ZCommutative (negSucc (succ a)) (nonneg b)) (transitivity (transitivity (applyEquality (λ i → nonneg b +Z negSucc (succ i)) (equalityCommutative (Semiring.sumZeroRight ℕSemiring a))) (+ZAssociative (nonneg b) (negSucc a) (negSucc 0))) (applyEquality (_+Z negSucc 0) (+ZCommutative (nonneg b) (negSucc a))))
++ZAssociative (negSucc (succ a)) (nonneg (succ b)) (negSucc (succ c)) = transitivity (+ZCommutative (negSucc (succ a)) (nonneg b +Z negSucc c)) (transitivity (transitivity (equalityCommutative (+ZAssociative (nonneg b) (negSucc c) (negSucc (succ a)))) (transitivity (applyEquality (λ i → nonneg b +Z negSucc i) (Semiring.commutative ℕSemiring (succ c) (succ a))) (+ZAssociative (nonneg b) (negSucc a) (negSucc (succ c))))) (applyEquality (_+Z negSucc (succ c)) (+ZCommutative (nonneg b) (negSucc a))))
++ZAssociative (negSucc a) (negSucc b) (nonneg zero) = refl
++ZAssociative (negSucc a) (negSucc zero) (nonneg (succ c)) = applyEquality (λ i → negSucc i +Z nonneg c) (Semiring.commutative ℕSemiring 0 a)
++ZAssociative (negSucc a) (negSucc (succ b)) (nonneg (succ c)) = transitivity (+ZAssociative (negSucc a) (negSucc b) (nonneg c)) (applyEquality (λ i → negSucc i +Z nonneg c) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a b)) (Semiring.commutative ℕSemiring (succ b) a)))
++ZAssociative (negSucc a) (negSucc b) (negSucc c) = applyEquality (λ i → negSucc (succ i)) (transitivity (Semiring.+Associative ℕSemiring a (succ b) c) (applyEquality (_+N c) (transitivity (Semiring.commutative ℕSemiring a (succ b)) (applyEquality succ (Semiring.commutative ℕSemiring b a)))))
+
+additiveInverseExists : (a : ℕ) → (negSucc a +Z nonneg (succ a)) ≡ nonneg 0
+additiveInverseExists zero = refl
+additiveInverseExists (succ a) = additiveInverseExists a
+
+additiveInverse : (a : ℤ) → ℤ
+additiveInverse (nonneg zero) = nonneg 0
+additiveInverse (nonneg (succ x)) = negSucc x
+additiveInverse (negSucc x) = nonneg (succ x)
+
+ℤGroup : Group (reflSetoid ℤ) (_+Z_)
+Group.wellDefined ℤGroup refl refl = refl
+Group.identity ℤGroup = nonneg 0
+Group.inverse ℤGroup = additiveInverse
+Group.multAssoc ℤGroup {a} {b} {c} = +ZAssociative a b c
+Group.multIdentRight ℤGroup {nonneg zero} = refl
+Group.multIdentRight ℤGroup {nonneg (succ x)} = applyEquality (λ i → nonneg (succ i)) (Semiring.commutative ℕSemiring x 0)
+Group.multIdentRight ℤGroup {negSucc x} = refl
+Group.multIdentLeft ℤGroup = refl
+Group.invLeft ℤGroup {nonneg zero} = refl
+Group.invLeft ℤGroup {nonneg (succ x)} = additiveInverseExists x
+Group.invLeft ℤGroup {negSucc x} = transitivity (+ZCommutative (nonneg (succ x)) (negSucc x)) (additiveInverseExists x)
+Group.invRight ℤGroup {nonneg zero} = refl
+Group.invRight ℤGroup {nonneg (succ x)} = transitivity (+ZCommutative (nonneg (succ x)) (negSucc x)) (additiveInverseExists x)
+Group.invRight ℤGroup {negSucc x} = additiveInverseExists x
+
+ℤAbGrp : AbelianGroup ℤGroup
+ℤAbGrp = record { commutative = λ {a} {b} → +ZCommutative a b }
diff --git a/Numbers/Integers/Definition.agda b/Numbers/Integers/Definition.agda
new file mode 100644
index 0000000..73d5ca9
--- /dev/null
+++ b/Numbers/Integers/Definition.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Numbers.Naturals.Definition
+
+module Numbers.Integers.Definition where
+
+data ℤ : Set where
+  nonneg : ℕ → ℤ
+  negSucc : ℕ → ℤ
+
+data ℤSimple : Set where
+  negativeSucc : (a : ℕ) → ℤSimple
+  positiveSucc : (a : ℕ) → ℤSimple
+  zZero : ℤSimple
+
+convertZ : ℤ → ℤSimple
+convertZ (nonneg zero) = zZero
+convertZ (nonneg (succ x)) = positiveSucc x
+convertZ (negSucc x) = negativeSucc x
+
+convertZ' : ℤSimple → ℤ
+convertZ' (negativeSucc a) = negSucc a
+convertZ' (positiveSucc a) = nonneg (succ a)
+convertZ' zZero = nonneg 0
+
+zIsZ : (a : ℤ) → convertZ' (convertZ a) ≡ a
+zIsZ (nonneg zero) = refl
+zIsZ (nonneg (succ x)) = refl
+zIsZ (negSucc x) = refl
+
+zIsZ' : (a : ℤSimple) → convertZ (convertZ' a) ≡ a
+zIsZ' (negativeSucc a) = refl
+zIsZ' (positiveSucc a) = refl
+zIsZ' zZero = refl
diff --git a/Numbers/Integers/Integers.agda b/Numbers/Integers/Integers.agda
new file mode 100644
index 0000000..4ea3f8c
--- /dev/null
+++ b/Numbers/Integers/Integers.agda
@@ -0,0 +1,17 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Numbers.Integers.Definition
+open import Numbers.Integers.Addition
+open import Numbers.Integers.Multiplication
+open import Numbers.Integers.Order
+open import Groups.Definition
+
+module Numbers.Integers.Integers where
+
+open Numbers.Integers.Definition using (ℤ ; nonneg ; negSucc) public
+open Numbers.Integers.Addition using (_+Z_ ; ℤGroup ; ℤAbGrp) public
+open Numbers.Integers.Multiplication using (_*Z_ ; ℤIntDom ; ℤRing) public
+open Numbers.Integers.Order using (_<Z_ ; ℤOrderedRing) public
+
+_-Z_ : ℤ → ℤ → ℤ
+a -Z b = a +Z (Group.inverse ℤGroup b)
diff --git a/Numbers/Integers/Multiplication.agda b/Numbers/Integers/Multiplication.agda
new file mode 100644
index 0000000..b1b4281
--- /dev/null
+++ b/Numbers/Integers/Multiplication.agda
@@ -0,0 +1,199 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Numbers.Naturals.Naturals
+open import Numbers.Naturals.Multiplication
+open import Numbers.Integers.Definition
+open import Numbers.Integers.Addition
+open import Semirings.Definition
+open import Groups.Definition
+open import Rings.Definition
+open import Setoids.Setoids
+open import Rings.IntegralDomains
+
+module Numbers.Integers.Multiplication where
+
+infix 25 _*Z_
+_*Z_ : ℤ → ℤ → ℤ
+nonneg x *Z nonneg y = nonneg (x *N y)
+nonneg zero *Z negSucc y = nonneg zero
+nonneg (succ x) *Z negSucc y = negSucc ((succ x) *N y +N x)
+negSucc x *Z nonneg zero = nonneg zero
+negSucc x *Z nonneg (succ y) = negSucc ((succ y) *N x +N y)
+negSucc x *Z negSucc y = nonneg ((succ x) *N (succ y))
+
+*ZInherits : (a b : ℕ) → nonneg (a *N b) ≡ (nonneg a) *Z (nonneg b)
+*ZInherits a b = refl
+
+*ZCommutative : (a b : ℤ) → a *Z b ≡ b *Z a
+*ZCommutative (nonneg x) (nonneg y) = applyEquality nonneg (multiplicationNIsCommutative x y)
+*ZCommutative (nonneg zero) (negSucc y) = refl
+*ZCommutative (nonneg (succ x)) (negSucc y) = refl
+*ZCommutative (negSucc x) (nonneg zero) = refl
+*ZCommutative (negSucc x) (nonneg (succ y)) = refl
+*ZCommutative (negSucc x) (negSucc y) = applyEquality nonneg (multiplicationNIsCommutative (succ x) (succ y))
+
+*ZleftIdent : (a : ℤ) → (nonneg 1) *Z a ≡ a
+*ZleftIdent (nonneg x) = applyEquality nonneg (Semiring.commutative ℕSemiring x 0)
+*ZleftIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
+
+*ZrightIdent : (a : ℤ) → a *Z (nonneg 1) ≡ a
+*ZrightIdent (nonneg x) = applyEquality nonneg (Semiring.productOneRight ℕSemiring x)
+*ZrightIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
+
+*ZZeroLeft : (a : ℤ) → nonneg 0 *Z a ≡ nonneg 0
+*ZZeroLeft (nonneg x) = refl
+*ZZeroLeft (negSucc x) = refl
+
+*ZZeroRight : (a : ℤ) → a *Z nonneg 0 ≡ nonneg 0
+*ZZeroRight (nonneg x) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring x)
+*ZZeroRight (negSucc x) = refl
+
+*ZAssociative : (a b c : ℤ) → a *Z (b *Z c) ≡ (a *Z b) *Z c
+*ZAssociative (nonneg zero) b c = transitivity (*ZZeroLeft (b *Z c)) (transitivity (equalityCommutative (*ZZeroLeft c)) (applyEquality (_*Z c) (equalityCommutative (*ZZeroLeft b))))
+*ZAssociative (nonneg (succ a)) (nonneg zero) c rewrite Semiring.productZeroRight ℕSemiring a | *ZZeroLeft c | Semiring.productZeroRight ℕSemiring a = refl
+*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring b | Semiring.productZeroRight ℕSemiring (b +N a *N succ b) | Semiring.productZeroRight ℕSemiring a = refl
+*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg (succ c)) = applyEquality nonneg (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
+*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc x) rewrite productDistributes' b (a *N succ b) x | Semiring.+Associative ℕSemiring x (b *N x) ((a *N succ b) *N x) | equalityCommutative (Semiring.+Associative ℕSemiring ((x +N b *N x) +N b) (a *N ((x +N b *N x) +N b)) a) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) ((a *N succ b) *N x) (b +N a *N succ b)) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) b (a *N ((x +N b *N x) +N b) +N a)) = applyEquality (λ i → negSucc ((x +N b *N x) +N i)) ans
+  where
+    ans3 : (succ b +N (succ b *N x)) *N a ≡ succ x *N (a *N succ b)
+    ans3 rewrite multiplicationNIsCommutative (succ b) x = transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a))
+    ans2 : a *N ((x +N b *N x) +N b) +N a ≡ (a *N succ b) +N (a *N succ b) *N x
+    ans2 rewrite multiplicationNIsCommutative (a *N succ b) x | Semiring.commutative ℕSemiring (succ b *N x) b | multiplicationNIsCommutative a (b +N (succ b *N x)) | Semiring.commutative ℕSemiring ((b +N (succ b *N x)) *N a) a = ans3
+    ans : b +N (a *N ((x +N b *N x) +N b) +N a) ≡ (a *N succ b) *N x +N (b +N a *N succ b)
+    ans rewrite Semiring.commutative ℕSemiring ((a *N succ b) *N x) (b +N a *N succ b) | equalityCommutative (Semiring.+Associative ℕSemiring b (a *N succ b) ((a *N succ b) *N x)) = applyEquality (b +N_) ans2
+*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg zero) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring a)
+*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg (succ c)) = applyEquality negSucc ans
+  where
+    ans4 : (b +N b *N c) +N (a *N b +N (a *N b) *N c) ≡ (b +N a *N b) +N (b *N c +N (a *N b) *N c)
+    ans4 rewrite Semiring.+Associative ℕSemiring (b +N b *N c) (a *N b) ((a *N b) *N c) | Semiring.+Associative ℕSemiring (b +N a *N b) (b *N c) ((a *N b) *N c) = applyEquality (_+N (a *N b) *N c) (transitivity (transitivity (applyEquality (_+N a *N b) (Semiring.commutative ℕSemiring b (b *N c))) (equalityCommutative (Semiring.+Associative ℕSemiring (b *N c) b (a *N b)))) (Semiring.commutative ℕSemiring (b *N c) (b +N a *N b)))
+    ans3 : ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) +N ((c +N a *N c) +N a) ≡ ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) +N ((a +N a *N c) +N c)
+    ans3 rewrite Semiring.commutative ℕSemiring (c +N a *N c) a | Semiring.commutative ℕSemiring c (a *N c) | Semiring.+Associative ℕSemiring a (a *N c) c = applyEquality (λ i → i +N ((a +N a *N c) +N c)) {(b +N b *N c) +N (a *N b +N (a *N b) *N c)} {(b +N a *N b) +N (b *N c +N (a *N b) *N c)} ans4
+    ans2 : (((b +N c *N b) +N (a *N b +N a *N (c *N b))) +N (c +N a *N c)) +N a ≡ (((b +N a *N b) +N (c *N b +N c *N (a *N b))) +N (a +N c *N a)) +N c
+    ans2 rewrite multiplicationNIsCommutative c b | multiplicationNIsCommutative c (a *N b) | Semiring.*Associative ℕSemiring a b c | multiplicationNIsCommutative c a = transitivity (equalityCommutative (Semiring.+Associative ℕSemiring ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) (c +N a *N c) a)) (transitivity ans3 (Semiring.+Associative ℕSemiring ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) (a +N a *N c) c))
+    ans : succ a *N ((succ c *N b) +N c) +N a ≡ succ c *N ((succ a *N b) +N a) +N c
+    ans = transitivity (applyEquality (_+N a) (productDistributes (succ a) (succ c *N b) c)) (transitivity (transitivity (applyEquality (λ i → ((((b +N c *N b) +N i) +N (c +N a *N c)) +N a)) (productDistributes a b (c *N b))) (transitivity ans2 (applyEquality (λ i → (((b +N a *N b) +N i) +N (a +N c *N a)) +N c) (equalityCommutative (productDistributes c b (a *N b)))))) (applyEquality (_+N c) (equalityCommutative (productDistributes (succ c) (succ a *N b) a))))
+*ZAssociative (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality nonneg ans
+  where
+    ans : succ a *N (succ b *N succ x) ≡ succ ((succ a *N b) +N a) *N succ x
+    ans rewrite Semiring.commutative ℕSemiring (succ a *N b) a | multiplicationNIsCommutative (succ a) b = transitivity (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)) (applyEquality (_*N succ x) {succ a *N succ b} {succ b *N succ a} (multiplicationNIsCommutative (succ a) (succ b)))
+*ZAssociative (negSucc a) (nonneg zero) c rewrite *ZZeroLeft c = refl
+*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite multiplicationNIsCommutative b 0 = refl
+*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc ans
+  where
+    ans2 : (d : ℕ) → ((succ b *N d) *N a) +N b *N d ≡ d *N ((succ b *N a) +N b)
+    ans2 d = transitivity (transitivity (applyEquality (((d +N b *N d) *N a) +N_) (multiplicationNIsCommutative b d)) (applyEquality (_+N d *N b) (transitivity (applyEquality (_*N a) {d +N b *N d} {d *N succ b} (multiplicationNIsCommutative (succ b) d)) (equalityCommutative (Semiring.*Associative ℕSemiring d (succ b) a))))) (equalityCommutative (Semiring.+DistributesOver* ℕSemiring d (succ b *N a) b))
+    ans : (succ (c +N b *N succ c) *N a) +N (c +N b *N succ c) ≡ (succ c *N ((succ b *N a) +N b)) +N c
+    ans rewrite Semiring.commutative ℕSemiring c (b *N succ c) | Semiring.+Associative ℕSemiring (succ (b *N succ c +N c) *N a) (b *N succ c) c | Semiring.commutative ℕSemiring (b *N succ c) c = applyEquality (_+N c) (ans2 (succ c))
+*ZAssociative (negSucc a) (nonneg (succ b)) (negSucc c) = applyEquality nonneg ans
+  where
+    ans : succ a *N ((succ ((succ b) *N c)) +N b) ≡ (succ (succ b *N a) +N b) *N succ c
+    ans rewrite Semiring.commutative ℕSemiring (succ b *N a) b | multiplicationNIsCommutative (succ b) a = transitivity (applyEquality (succ a *N_) (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring c (b *N c) b)) (applyEquality (c +N_) (transitivity (transitivity (Semiring.commutative ℕSemiring (b *N c) b) (applyEquality (b +N_) (multiplicationNIsCommutative b c))) (multiplicationNIsCommutative (succ c) b)))))) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
+*ZAssociative (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring (b +N a *N succ b) = refl
+*ZAssociative (negSucc a) (negSucc b) (nonneg (succ x)) = applyEquality nonneg (transitivity (applyEquality (succ a *N_) ans) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)))
+  where
+    ans : succ ((succ x *N b) +N x) ≡ (succ b *N succ x)
+    ans rewrite Semiring.commutative ℕSemiring (succ x *N b) x | multiplicationNIsCommutative (succ x) b = refl
+*ZAssociative (negSucc a) (negSucc b) (negSucc x) = applyEquality negSucc t
+  where
+    l1 : (a b c d e f g : ℕ) → (a +N b) +N d ≡ e +N (f +N g) → (a +N b) +N (c +N d) ≡ (c +N e) +N (f +N g)
+    l1 a b c d e f g pr rewrite Semiring.commutative ℕSemiring c d | Semiring.+Associative ℕSemiring (a +N b) d c | pr | Semiring.commutative ℕSemiring (e +N (f +N g)) c | Semiring.+Associative ℕSemiring c e (f +N g) = refl
+    v : (((succ b) *N succ x) *N a) ≡ (succ x) *N (a *N succ b)
+    v = transitivity (applyEquality (_*N a) (multiplicationNIsCommutative (succ b) (succ x))) (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a)))
+    u : (a +N (x +N b *N succ x) *N a) +N b *N succ x ≡ (b +N a *N succ b) *N x +N (b +N a *N succ b)
+    u = transitivity (transitivity (transitivity (Semiring.commutative ℕSemiring (a +N (x +N b *N succ x) *N a) (b *N succ x)) (transitivity (applyEquality (_+N (a +N (x +N b *N succ x) *N a)) (multiplicationNIsCommutative b (succ x))) (transitivity (applyEquality ((b +N x *N b) +N_) v) (equalityCommutative (productDistributes (succ x) b (a *N succ b)))))) (applyEquality ((b +N a *N succ b) +N_) (multiplicationNIsCommutative x (b +N a *N succ b)))) (Semiring.commutative ℕSemiring (b +N a *N succ b) ((b +N a *N succ b) *N x))
+    t : (a +N (x +N b *N succ x) *N a) +N (x +N b *N succ x) ≡ (x +N (b +N a *N succ b) *N x) +N (b +N a *N succ b)
+    t = l1 a ((x +N b *N succ x) *N a) x (b *N succ x) ((b +N (a *N succ b)) *N x) b (a *N succ b) u
+
+multLemma : (a b : ℕ) → a *N succ b ≡ a *N b +N a
+multLemma a b rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative a b = refl
+
+negSucc+Nonneg : (a b : ℕ) → negSucc a ≡ negSucc (a +N b) +Z nonneg b
+negSucc+Nonneg zero zero = refl
+negSucc+Nonneg zero (succ b) = negSucc+Nonneg zero b
+negSucc+Nonneg (succ a) zero rewrite Semiring.commutative ℕSemiring a 0 = refl
+negSucc+Nonneg (succ a) (succ b) rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring b a = negSucc+Nonneg (succ a) b
+
+distLemma : (a b : ℕ) →  negSucc a *Z nonneg b ≡ negSucc ((a +N b *N a) +N b) +Z nonneg (succ a)
+distLemma a b rewrite Semiring.commutative ℕSemiring (a +N b *N a) b | Semiring.commutative ℕSemiring a (b *N a) | Semiring.+Associative ℕSemiring b (b *N a) a = transitivity u (transitivity (equalityCommutative (+ZAssociative (negSucc ((b +N b *N a) +N a)) (nonneg a) (nonneg 1))) (applyEquality ((negSucc ((b +N b *N a) +N a)) +Z_) {nonneg a +Z nonneg 1} {nonneg (succ a)} (+ZCommutative (nonneg a) (nonneg 1))))
+  where
+    v : (a b : ℕ) → negSucc a *Z nonneg b ≡ (negSucc (b +N b *N a)) +Z nonneg 1
+    v zero zero = refl
+    v zero (succ b) rewrite Semiring.productZeroRight ℕSemiring b = applyEquality negSucc (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))
+    v (succ a) zero = refl
+    v (succ a) (succ b) = applyEquality negSucc (Semiring.commutative ℕSemiring (succ (a +N b *N succ a)) b)
+    u : negSucc a *Z nonneg b ≡ (negSucc ((b +N b *N a) +N a) +Z nonneg a) +Z nonneg 1
+    u = transitivity (v a b) (applyEquality (_+Z nonneg 1) (negSucc+Nonneg (b +N b *N a) a))
+
+*ZDistributesOver+Z : (a b c : ℤ) → a *Z (b +Z c) ≡ (a *Z b) +Z (a *Z c)
+*ZDistributesOver+Z (nonneg zero) b c rewrite *ZZeroLeft (b +Z c) | *ZZeroLeft b | *ZZeroLeft c = refl
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (nonneg c) rewrite Semiring.productZeroRight ℕSemiring a = refl
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (nonneg c) = applyEquality nonneg (productDistributes (succ a) (succ b) c)
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (negSucc c) rewrite Semiring.productZeroRight ℕSemiring a = refl
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productZeroRight ℕSemiring a = t a
+  where
+    t : (a : ℕ) → nonneg (succ a *N b) ≡ nonneg (succ a *N succ b) +Z negSucc a
+    t zero = refl
+    t (succ a) = transitivity (+Zinherits b (b +N a *N b)) (transitivity (applyEquality (nonneg b +Z_) (t a)) (transitivity (+ZAssociative (nonneg b) (nonneg (succ (b +N a *N succ b))) (negSucc a)) (applyEquality (_+Z negSucc a) {nonneg b +Z nonneg (succ (b +N a *N succ b))} {nonneg (b +N succ (b +N a *N succ b))} (equalityCommutative (+Zinherits b _)))))
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ x)) (negSucc (succ b)) = transitivity (applyEquality ((nonneg (succ a)) *Z_) (+ZCommutative (nonneg x) (negSucc b))) (transitivity (transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t) (+ZCommutative (negSucc ((b +N a *N succ b) +N a)) (nonneg (x +N a *N succ x))))
+  where
+    t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
+    t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
+*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring a = refl
+*ZDistributesOver+Z (nonneg (succ a)) (negSucc zero) (nonneg (succ x)) rewrite Semiring.productZeroRight ℕSemiring a = t a x
+  where
+    t : (a x : ℕ) → nonneg (succ a *N x) ≡ negSucc a +Z nonneg (succ a *N succ x)
+    t zero x = refl
+    t (succ a) x with t a x
+    ... | bl rewrite +Zinherits x (a *N x) | +Zinherits x (x +N a *N x) = transitivity (transitivity (applyEquality (nonneg x +Z_) (+Zinherits x (a *N x))) (+ZCommutative (nonneg x) (nonneg x +Z nonneg (a *N x)))) (transitivity (applyEquality (_+Z nonneg x) bl) (transitivity (equalityCommutative (+ZAssociative (negSucc a) (nonneg (succ x +N a *N succ x)) (nonneg x))) (applyEquality (λ i → negSucc a +Z nonneg i) {succ (x +N a *N succ x) +N x} {x +N succ (x +N a *N succ x)} (Semiring.commutative ℕSemiring (succ (x +N a *N succ x)) x))))
+*ZDistributesOver+Z (nonneg (succ a)) (negSucc (succ b)) (nonneg (succ x)) = transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t
+  where
+    t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
+    t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
+*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality negSucc (transitivity (applyEquality (_+N a) (transitivity (productDistributes (succ a) (succ b) x) (applyEquality (_+N (x +N a *N x)) {succ b +N a *N succ b} {succ (b +N a *N b) +N a} (applyEquality succ u)))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ ((b +N a *N b) +N a)) (succ a *N x) a)))
+  where
+    u : b +N a *N succ b ≡ (succ a *N b) +N a
+    u rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative b a = Semiring.+Associative ℕSemiring b (a *N b) a
+*ZDistributesOver+Z (negSucc a) (nonneg zero) (nonneg x) = refl
+*ZDistributesOver+Z (negSucc a) (nonneg zero) (negSucc x) = refl
+*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite Semiring.commutative ℕSemiring b 0 = refl
+*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc t
+  where
+    v : a *N b +N a *N succ c ≡ c *N a +N (a +N b *N a)
+    v rewrite multiplicationNIsCommutative b a | Semiring.+Associative ℕSemiring (c *N a) a (a *N b) | Semiring.commutative ℕSemiring (c *N a +N a) (a *N b) | Semiring.commutative ℕSemiring (c *N a) a = applyEquality (λ i → a *N b +N i) (transitivity (multLemma a c) (transitivity (Semiring.commutative ℕSemiring (a *N c) a) (applyEquality (a +N_) (multiplicationNIsCommutative a c))))
+    u : (a +N (b +N succ c) *N a) +N b ≡ (a +N c *N a) +N ((a +N b *N a) +N b)
+    u rewrite Semiring.+Associative ℕSemiring (a +N c *N a) (a +N b *N a) b | (equalityCommutative (Semiring.+Associative ℕSemiring a (c *N a) (a +N b *N a))) = applyEquality (λ i → (a +N i) +N b) (transitivity (multiplicationNIsCommutative (b +N succ c) a) (transitivity (productDistributes a b (succ c)) v))
+    t : (a +N (b +N succ c) *N a) +N (b +N succ c) ≡ succ (((a +N b *N a) +N b) +N ((a +N c *N a) +N c))
+    t rewrite Semiring.+Associative ℕSemiring ((a +N (b +N succ c) *N a)) b (succ c) | Semiring.commutative ℕSemiring ((a +N b *N a) +N b) ((a +N c *N a) +N c) | Semiring.commutative ℕSemiring (a +N c *N a) c | equalityCommutative (Semiring.+Associative ℕSemiring (succ c) (a +N c *N a) ((a +N b *N a) +N b)) | Semiring.commutative ℕSemiring (succ c) ((a +N c *N a) +N ((a +N b *N a) +N b)) = applyEquality (_+N succ c) u
+*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productOneRight ℕSemiring a = distLemma a b
+*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc (succ c)) = transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))
+  where
+    t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
+    t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
+*ZDistributesOver+Z (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.commutative ℕSemiring (b +N a *N succ b) 0 = refl
+*ZDistributesOver+Z (negSucc a) (negSucc zero) (nonneg (succ b)) = transitivity (distLemma a b) (transitivity (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a))) (applyEquality (λ i → nonneg (succ i) +Z negSucc ((a +N b *N a) +N b)) (equalityCommutative (Semiring.productOneRight ℕSemiring a))))
+*ZDistributesOver+Z (negSucc a) (negSucc (succ c)) (nonneg (succ b)) = transitivity (applyEquality (negSucc a *Z_) (+ZCommutative (negSucc c) (nonneg b))) (transitivity (transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))) (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ (succ (c +N a *N succ (succ c)))))))
+  where
+    t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
+    t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
+*ZDistributesOver+Z (negSucc a) (negSucc b) (negSucc c) = applyEquality nonneg (transitivity (applyEquality (λ i → succ a *N (succ i)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring b c)) (Semiring.commutative ℕSemiring (succ c) b))) (productDistributes (succ a) (succ b) (succ c)))
+
+ℤRing : Ring (reflSetoid ℤ) _+Z_ _*Z_
+Ring.additiveGroup ℤRing = ℤGroup
+Ring.multWellDefined ℤRing refl refl = refl
+Ring.1R ℤRing = nonneg 1
+Ring.groupIsAbelian ℤRing {a} {b} = +ZCommutative a b
+Ring.multAssoc ℤRing {a} {b} {c} = *ZAssociative a b c
+Ring.multCommutative ℤRing {a} {b} = *ZCommutative a b
+Ring.multDistributes ℤRing {a} {b} {c} = *ZDistributesOver+Z a b c
+Ring.multIdentIsIdent ℤRing {a} = *ZleftIdent a
+
+intDom : (a b : ℤ) → a *Z b ≡ nonneg 0 → (a ≡ nonneg 0) || (b ≡ nonneg 0)
+intDom (nonneg zero) (nonneg b) pr = inl refl
+intDom (nonneg (succ a)) (nonneg zero) pr = inr refl
+intDom (nonneg zero) (negSucc b) pr = inl refl
+intDom (negSucc a) (nonneg zero) pr = inr refl
+
+ℤIntDom : IntegralDomain ℤRing
+IntegralDomain.intDom ℤIntDom {a} {b} = intDom a b
+IntegralDomain.nontrivial ℤIntDom ()
diff --git a/Numbers/Integers/Order.agda b/Numbers/Integers/Order.agda
new file mode 100644
index 0000000..5a8cc8a
--- /dev/null
+++ b/Numbers/Integers/Order.agda
@@ -0,0 +1,99 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Numbers.Naturals.Naturals
+open import Numbers.Integers.Definition
+open import Numbers.Integers.Addition
+open import Numbers.Integers.Multiplication
+open import Semirings.Definition
+open import Rings.Definition
+open import Setoids.Setoids
+open import Setoids.Orders
+open import Orders
+
+module Numbers.Integers.Order where
+
+infix 5 _<Z_
+record _<Z_ (a : ℤ) (b : ℤ) : Set where
+  constructor le
+  field
+    x : ℕ
+    proof : (nonneg (succ x)) +Z a ≡ b
+
+lessLemma : (a x : ℕ) → succ x +N a ≡ a → False
+lessLemma zero x pr = naughtE (equalityCommutative pr)
+lessLemma (succ a) x pr = lessLemma a x q
+  where
+    q : succ x +N a ≡ a
+    q rewrite Semiring.commutative ℕSemiring a (succ x) | Semiring.commutative ℕSemiring x a | Semiring.commutative ℕSemiring (succ a) x = succInjective pr
+
+nonnegInjective : {a b : ℕ} → (nonneg a ≡ nonneg b) → (a ≡ b)
+nonnegInjective {a} {.a} refl = refl
+
+irreflexive : (x : ℤ) → x <Z x → False
+irreflexive (nonneg x) record { x = y ; proof = proof } = lessLemma x y (nonnegInjective proof)
+irreflexive (negSucc a) record { x = x ; proof = proof } = naughtE (equalityCommutative q)
+  where
+    pr' : nonneg (succ x) +Z (negSucc a +Z nonneg (succ a)) ≡ negSucc a +Z nonneg (succ a)
+    pr' rewrite +ZAssociative (nonneg (succ x)) (negSucc a) (nonneg (succ a)) = applyEquality (λ t → t +Z nonneg (succ a)) proof
+    pr'' : nonneg (succ x) +Z nonneg 0 ≡ nonneg 0
+    pr'' rewrite equalityCommutative (additiveInverseExists a) = identityOfIndiscernablesLeft (nonneg (succ x) +Z (negSucc a +Z nonneg (succ a))) (negSucc a +Z nonneg (succ a)) (nonneg (succ (x +N zero))) _≡_ pr' q
+      where
+        q : nonneg (succ x) +Z (negSucc a +Z nonneg (succ a)) ≡ nonneg (succ (x +N 0))
+        q rewrite Semiring.commutative ℕSemiring x 0 | additiveInverseExists a | Semiring.commutative ℕSemiring x 0 = refl
+    pr''' : succ x +N 0 ≡ 0
+    pr''' = nonnegInjective pr''
+    q : succ x ≡ 0
+    q rewrite Semiring.commutative ℕSemiring 0 (succ x) = pr'''
+
+lessZTransitive : {a b c : ℤ} → (a <Z b) → (b <Z c) → (a <Z c)
+lessZTransitive {a} {b} {c} (le d1 pr1) (le d2 pr2) rewrite equalityCommutative pr1 = le (d1 +N succ d2) pr
+  where
+    pr : nonneg (succ (d1 +N succ d2)) +Z a ≡ c
+    pr rewrite +ZAssociative (nonneg (succ d2)) (nonneg (succ d1)) a | Semiring.commutative ℕSemiring (succ d2) (succ d1) = pr2
+
+lessInherits : {a b : ℕ} → (a <N b) → ((nonneg a) <Z (nonneg b))
+_<Z_.x (lessInherits {a} {b} (le x proof)) = x
+_<Z_.proof (lessInherits {a} {.(succ (x +N a))} (le x refl)) = refl
+
+lessInheritsNegsucc : {a b : ℕ} → (a <N b) → ((negSucc b) <Z negSucc a)
+_<Z_.x (lessInheritsNegsucc {a} {b} (le x proof)) = x
+_<Z_.proof (lessInheritsNegsucc {a} {b} (le x proof)) rewrite equalityCommutative proof = transitivity (transitivity (+ZCommutative (nonneg x) (negSucc (x +N a))) (applyEquality (λ i → negSucc i +Z nonneg x) (Semiring.commutative ℕSemiring x a))) (equalityCommutative (negSucc+Nonneg a x))
+
+lessNegsuccNonneg : {a b : ℕ} → (negSucc a <Z nonneg b)
+_<Z_.x (lessNegsuccNonneg {a} {b}) = a +N b
+_<Z_.proof (lessNegsuccNonneg {zero} {b}) = refl
+_<Z_.proof (lessNegsuccNonneg {succ a} {b}) = _<Z_.proof (lessNegsuccNonneg {a} {b})
+
+lessThanTotalZ : {a b : ℤ} → ((a <Z b) || (b <Z a)) || (a ≡ b)
+lessThanTotalZ {nonneg a} {nonneg b} with orderIsTotal a b
+lessThanTotalZ {nonneg a} {nonneg b} | inl (inl a<b) = inl (inl (lessInherits a<b))
+lessThanTotalZ {nonneg a} {nonneg b} | inl (inr b<a) = inl (inr (lessInherits b<a))
+lessThanTotalZ {nonneg a} {nonneg b} | inr a=b = inr (applyEquality nonneg a=b)
+lessThanTotalZ {nonneg a} {negSucc b} = inl (inr (lessNegsuccNonneg {b} {a}))
+lessThanTotalZ {negSucc a} {nonneg x} = inl (inl (lessNegsuccNonneg {a} {x}))
+lessThanTotalZ {negSucc a} {negSucc b} with orderIsTotal a b
+... | inl (inl a<b) = inl (inr (lessInheritsNegsucc a<b))
+... | inl (inr b<a) = inl (inl (lessInheritsNegsucc b<a))
+lessThanTotalZ {negSucc a} {negSucc .a} | inr refl = inr refl
+
+ℤOrder : TotalOrder ℤ
+PartialOrder._<_ (TotalOrder.order ℤOrder) = _<Z_
+PartialOrder.irreflexive (TotalOrder.order ℤOrder) {a} = irreflexive a
+PartialOrder.transitive (TotalOrder.order ℤOrder) = lessZTransitive
+TotalOrder.totality ℤOrder a b = lessThanTotalZ {a} {b}
+
+orderRespectsAddition : (a b : ℤ) → a <Z b → (c : ℤ) → a +Z c <Z b +Z c
+orderRespectsAddition (nonneg a) (nonneg b) (le x proof) (nonneg c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (nonneg a) (nonneg c)) (applyEquality (_+Z nonneg c) proof))
+orderRespectsAddition (nonneg a) (nonneg b) (le x proof) (negSucc c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (nonneg a) (negSucc c)) (applyEquality (_+Z negSucc c) proof))
+orderRespectsAddition (negSucc a) (nonneg b) (le x proof) (nonneg c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (negSucc a) (nonneg c)) (applyEquality (_+Z nonneg c) proof))
+orderRespectsAddition (negSucc a) (nonneg b) (le x proof) (negSucc c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (negSucc a) (negSucc c)) (applyEquality (_+Z negSucc c) proof))
+orderRespectsAddition (negSucc a) (negSucc b) (le x proof) (nonneg c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (negSucc a) (nonneg c)) (applyEquality (_+Z nonneg c) proof))
+orderRespectsAddition (negSucc a) (negSucc b) (le x proof) (negSucc c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (negSucc a) (negSucc c)) (applyEquality (_+Z negSucc c) proof))
+
+orderRespectsMultiplication : (a b : ℤ) → nonneg 0 <Z a → nonneg 0 <Z b → nonneg 0 <Z a *Z b
+orderRespectsMultiplication (nonneg (succ a)) (nonneg (succ b)) 0<a 0<b = lessInherits (succIsPositive (b +N a *N succ b))
+
+ℤOrderedRing : OrderedRing ℤRing (totalOrderToSetoidTotalOrder ℤOrder)
+OrderedRing.orderRespectsAddition ℤOrderedRing {a} {b} = orderRespectsAddition a b
+OrderedRing.orderRespectsMultiplication ℤOrderedRing {a} {b} = orderRespectsMultiplication a b
diff --git a/Numbers/Rationals.agda b/Numbers/Rationals.agda
index ed3c06b..62b6e64 100644
--- a/Numbers/Rationals.agda
+++ b/Numbers/Rationals.agda
@@ -2,7 +2,7 @@
 
 open import LogicalFormulae
 open import Numbers.Naturals.Naturals
-open import Numbers.Integers
+open import Numbers.Integers.Integers
 open import Groups.Groups
 open import Groups.Definition
 open import Rings.Definition
diff --git a/Numbers/RationalsLemmas.agda b/Numbers/RationalsLemmas.agda
index 5380c13..8db2236 100644
--- a/Numbers/RationalsLemmas.agda
+++ b/Numbers/RationalsLemmas.agda
@@ -2,7 +2,7 @@
 
 open import LogicalFormulae
 open import Numbers.Naturals.Naturals
-open import Numbers.Integers
+open import Numbers.Integers.Integers
 open import Numbers.Rationals
 open import Groups.Groups
 open import Groups.Lemmas
diff --git a/Rings/Examples/Examples.agda b/Rings/Examples/Examples.agda
index 93966c1..edb45fc 100644
--- a/Rings/Examples/Examples.agda
+++ b/Rings/Examples/Examples.agda
@@ -4,7 +4,7 @@ open import LogicalFormulae
 open import Groups.Groups
 open import Functions
 open import Numbers.Naturals.Naturals
-open import Numbers.Integers
+open import Numbers.Integers.Integers
 open import IntegersModN
 open import Rings.Examples.Proofs
 open import PrimeNumbers
diff --git a/Rings/Examples/Proofs.agda b/Rings/Examples/Proofs.agda
index b50ab59..1fd1572 100644
--- a/Rings/Examples/Proofs.agda
+++ b/Rings/Examples/Proofs.agda
@@ -7,7 +7,7 @@ open import Groups.Definition
 open import Orders
 open import Rings.Definition
 open import Numbers.Naturals.Naturals
-open import Numbers.Integers
+open import Numbers.Integers.Integers
 open import PrimeNumbers
 open import IntegersModN