```module Qtest where

open import Data.Nat
open import Data.Nat.Properties as Nat
open import Relation.Binary
open import Quotient
open import Data.Product
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open ≡-Reasoning
open Nat.SemiringSolver

Int : Setoid _ _
Int = record
{ Carrier       = ℕ × ℕ
; _≈_           = λ { (x+ , x-) (y+ , y-) → x+ + y- ≡ y+ + x- }
; isEquivalence = record
{ refl  = λ {_} → refl
; sym   = λ p → sym p
; trans = λ { {x+ , x-}{y+ , y-}{z+ , z-} p q →
cancel-+-left (y- + y+) (begin
(y- + y+) + (x+ + z-)  ≡⟨ solve 4 (λ y- y+ x+ z- → (y- :+ y+) :+ (x+ :+ z-) :=
x+ :+ y- :+ (y+ :+ z-))
refl y- y+ x+ z- ⟩
x+ + y- + (y+ + z-)    ≡⟨ cong₂ _+_ p q ⟩
y+ + x- + (z+ + y-)    ≡⟨ solve 4 (λ y+ x- z+ y- → y+ :+ x- :+ (z+ :+ y-) :=
(y- :+ y+) :+ (z+ :+ x-))
refl y+ x- z+ y- ⟩
(y- + y+) + (z+ + x-)  ∎) }
}
}

ℤ : Set
ℤ = Quotient Int

zeroℤ : ℤ
zeroℤ = [ 0 , 0 ]

open import Algebra
module CS = CommutativeSemiring Nat.commutativeSemiring

minus : ℤ → ℤ
minus x = rec {A = Int}
ℤ
(λ {(x+ , x-) → [ x- , x+ ]})
(λ { {x+ , x-} {y+ , y-} x≈y → [ sym (trans (CS.+-comm y- x+)
(trans x≈y
(CS.+-comm y+ x-))) ]-cong})
x

minus-lem : (x : ℤ) → minus (minus x) ≡ x
minus-lem x = elim {A = Int} (λ x → minus (minus x) ≡ x)
(λ { (x+ , x-) → refl}) (λ x≈y → proof-irrelevance _ _) x

```