```------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to addition of integers
------------------------------------------------------------------------

open import Algebra
import Algebra.FunctionProperties
open import Algebra.Structures
open import Data.Integer hiding (suc)
open import Data.Nat using (suc; zero) renaming (_+_ to _ℕ+_)
import Data.Nat.Properties as ℕ
open import Relation.Binary.PropositionalEquality

open Algebra.FunctionProperties (_≡_ {A = ℤ})
open CommutativeSemiring ℕ.commutativeSemiring
using (+-comm; +-assoc; +-identity)

------------------------------------------------------------------------
-- Addition and zero form a commutative monoid

private

comm : Commutative _+_
comm -[1+ a ] -[1+ b ] rewrite +-comm a b = refl
comm (+   a ) (+   b ) rewrite +-comm a b = refl
comm -[1+ _ ] (+   _ ) = refl
comm (+   _ ) -[1+ _ ] = refl

identityˡ : LeftIdentity (+ 0) _+_
identityˡ -[1+ _ ] = refl
identityˡ (+   _ ) = refl

identityʳ : RightIdentity (+ 0) _+_
identityʳ x rewrite comm x (+ 0) = identityˡ x

distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ+ a)
distribˡ-⊖-+-neg _ zero    zero    = refl
distribˡ-⊖-+-neg _ zero    (suc _) = refl
distribˡ-⊖-+-neg _ (suc _) zero    = refl
distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c

distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ+ c)
distribʳ-⊖-+-neg a b c
rewrite comm -[1+ a ] (b ⊖ c)
| distribˡ-⊖-+-neg a b c
| +-comm a c
= refl

distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ+ a ⊖ c
distribˡ-⊖-+-pos _ zero    zero    = refl
distribˡ-⊖-+-pos _ zero    (suc _) = refl
distribˡ-⊖-+-pos _ (suc _) zero    = refl
distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c

distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ+ b ⊖ c
distribʳ-⊖-+-pos a b c
rewrite comm (+ a) (b ⊖ c)
| distribˡ-⊖-+-pos a b c
| +-comm a b
= refl

assoc : Associative _+_
assoc (+ zero) y z rewrite identityˡ      y  | identityˡ (y + z) = refl
assoc x (+ zero) z rewrite identityʳ  x      | identityˡ      z  = refl
assoc x y (+ zero) rewrite identityʳ (x + y) | identityʳ  y      = refl
assoc -[1+ a ]  -[1+ b ]  (+ suc c) = sym (distribʳ-⊖-+-neg a c b)
assoc -[1+ a ]  (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a
assoc (+ suc a) -[1+ b ]  -[1+ c ]  = distribˡ-⊖-+-neg c a b
assoc (+ suc a) -[1+ b ] (+ suc c)
rewrite distribˡ-⊖-+-pos (suc c) a b
| distribʳ-⊖-+-pos (suc a) c b
| sym (+-assoc a 1 c)
| +-comm a 1
= refl
assoc (+ suc a) (+ suc b) -[1+ c ]
rewrite distribʳ-⊖-+-pos (suc a) b c
| sym (+-assoc a 1 b)
| +-comm a 1
= refl
assoc -[1+ a ] -[1+ b ] -[1+ c ]
rewrite sym (+-assoc a 1 (b ℕ+ c))
| +-comm a 1
| +-assoc a b c
= refl
assoc -[1+ a ] (+ suc b) -[1+ c ]
rewrite distribʳ-⊖-+-neg a b c
| distribˡ-⊖-+-neg c b a
= refl
assoc (+ suc a) (+ suc b) (+ suc c)
rewrite +-assoc (suc a) (suc b) (suc c)
= refl

isSemigroup : IsSemigroup _≡_ _+_
isSemigroup = record
{ isEquivalence = isEquivalence
; assoc         = assoc
; ∙-cong        = cong₂ _+_
}

isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ 0)
isCommutativeMonoid = record
{ isSemigroup = isSemigroup
; identityˡ   = identityˡ
; comm        = comm
}

commutativeMonoid : CommutativeMonoid _ _
commutativeMonoid = record
{ Carrier             = ℤ
; _≈_                 = _≡_
; _∙_                 = _+_
; ε                   = + 0
; isCommutativeMonoid = isCommutativeMonoid
}
```