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

module Data.Integer.Multiplication.Properties where

open import Algebra
using (module CommutativeSemiring; CommutativeMonoid)
import Algebra.FunctionProperties
open import Algebra.Structures using (IsSemigroup; IsCommutativeMonoid)
open import Data.Integer
using (ℤ; -[1+_]; +_; ∣_∣; sign; _◃_) renaming (_*_ to ℤ*)
open import Data.Nat
using (suc; zero) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Product using (proj₂)
import Data.Nat.Properties as ℕ
open import Data.Sign using () renaming (_*_ to _S*_)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; cong; cong₂; isEquivalence)

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

------------------------------------------------------------------------
-- Multiplication and one form a commutative monoid

private

identityˡ : LeftIdentity (+ 1) ℤ*
identityˡ (+ zero ) = refl
identityˡ -[1+  n ] rewrite proj₂ +-identity n = refl
identityˡ (+ suc n) rewrite proj₂ +-identity n = refl

comm : Commutative ℤ*
comm -[1+ a ] -[1+ b ] rewrite *-comm (suc a) (suc b) = refl
comm -[1+ a ] (+   b ) rewrite *-comm (suc a) b       = refl
comm (+   a ) -[1+ b ] rewrite *-comm a       (suc b) = refl
comm (+   a ) (+   b ) rewrite *-comm a       b       = refl

lemma : ∀ a b c → c ℕ+ (b ℕ+ a ℕ* suc b) ℕ* suc c
≡ c ℕ+ b ℕ* suc c ℕ+ a ℕ* suc (c ℕ+ b ℕ* suc c)
lemma =
solve 3 (λ a b c → c :+ (b :+ a :* (con 1 :+ b)) :* (con 1 :+ c)
:= c :+ b :* (con 1 :+ c) :+
a :* (con 1 :+ (c :+ b :* (con 1 :+ c))))
refl
where open ℕ.SemiringSolver

assoc : Associative ℤ*
assoc (+ zero) _ _ = refl
assoc x (+ zero) _ rewrite proj₂ *-zero ∣ x ∣ = refl
assoc x y (+ zero) rewrite
proj₂ *-zero ∣ y ∣
| proj₂ *-zero ∣ x ∣
| proj₂ *-zero ∣ sign x S* sign y ◃ ∣ x ∣ ℕ* ∣ y ∣ ∣
= refl
assoc -[1+ a  ] -[1+ b  ] (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
assoc -[1+ a  ] (+ suc b) -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
assoc (+ suc a) (+ suc b) (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
assoc (+ suc a) -[1+ b  ] -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
assoc -[1+ a  ] -[1+ b  ] -[1+ c  ] = cong -[1+_]     (lemma a b c)
assoc -[1+ a  ] (+ suc b) (+ suc c) = cong -[1+_]     (lemma a b c)
assoc (+ suc a) -[1+ b  ] (+ suc c) = cong -[1+_]     (lemma a b c)
assoc (+ suc a) (+ suc b) -[1+ c  ] = cong -[1+_]     (lemma a b c)

isSemigroup : IsSemigroup _ _
isSemigroup = record
{ isEquivalence = isEquivalence
; assoc         = assoc
; ∙-cong        = cong₂ ℤ*
}

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

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