```module MiniLibrary.Integer where

open import MiniLibrary.Base
open import MiniLibrary.Nat
open import MiniLibrary.Natplus

data ℤ : Set where
+_     :  ℕ+      → ℤ
zero   :  ℤ
-_     :  ℕ+     → ℤ

_<ℤb_ : ℤ → ℤ → Bool
(- n) <ℤb (- m) = m <ℕ+b n
(- n) <ℤb z     = true
zero  <ℤb (+ m) = true
zero  <ℤb z     = false
(+ n) <ℤb (+ m) = n <ℕ+b m
(+ n) <ℤb z     = false

_<ℤ_ : ℤ → ℤ → Set
n <ℤ m = True (n <ℤb m)

_≤ℤb_ : ℤ → ℤ → Bool
(- n) ≤ℤb (- m) = m ≤ℕ+b n
(- n) ≤ℤb z     = true
zero  ≤ℤb (- m) = false
zero  ≤ℤb z     = true
(+ n) ≤ℤb (+ m) = n ≤ℕ+b m
(+ n) ≤ℤb z     = false

_≤ℤ_ : ℤ → ℤ → Set
z ≤ℤ z' = True (z ≤ℤb z')

_≥ℤb_ : ℤ  -> ℤ  →  Bool
z ≥ℤb z' = z' ≤ℤb z

_≥ℤ_ : ℤ  -> ℤ  -> Set
z ≥ℤ z' = z' ≤ℤ z

_==ℤb_ : ℤ → ℤ → Bool
(- n) ==ℤb (- m) = m ==ℕ+b n
(- n) ==ℤb z     = false
zero  ==ℤb zero  = true
zero  ==ℤb z     = false
(+ n) ==ℤb (+ m) = n ==ℕ+b m
(+ n) ==ℤb z     = false

_==ℤ_ : ℤ → ℤ → Set
n ==ℤ m = True (n ==ℤb m)

decideℤ : (z z' : ℤ) → z <ℤ   z' ∨ z ==ℤ z' ∨ z' <ℤ z
decideℤ (- n) (- m) = decideℕ+ m n
decideℤ (- n) (+ _) = in0 triv
decideℤ (- n) zero  = in0 triv
decideℤ zero (+ _)  = in0 triv
decideℤ zero zero   = in1 triv
decideℤ zero (- _)  = in2 triv
decideℤ (+ n) (+ m) = decideℕ+ n m
decideℤ (+ n) zero  = in2 triv
decideℤ (+ n) (- _) = in2 triv

decideℤ≤ : (z z' : ℤ) → z ≤ℤ   z' ∨ z' ≤ℤ z
decideℤ≤ (- n) (- m) = decideℕ+≤ m n
decideℤ≤ (- n) (+ _) = inl triv
decideℤ≤ (- n) zero  = inl triv
decideℤ≤ zero (+ _) = inl triv
decideℤ≤ zero zero = inl triv
decideℤ≤ zero (- _) = inr triv
decideℤ≤ (+ n) (+ m) = decideℕ+≤ n m
decideℤ≤ (+ n) zero = inr triv
decideℤ≤ (+ n) (- _) = inr triv

_-ℕ2ℤ_ : ℕ → ℕ → ℤ
zero    -ℕ2ℤ zero  = zero
zero    -ℕ2ℤ suc n = - (suc n)
suc n   -ℕ2ℤ zero  = + (suc n)
suc n   -ℕ2ℤ suc m = n  -ℕ2ℤ m

minusℤ  : ℤ → ℤ
minusℤ (+ n)  = - n
minusℤ zero   = zero
minusℤ (- n)  = + n

_+ℤ_ : ℤ → ℤ → ℤ
z           +ℤ zero        = z
zero        +ℤ z           = z
(+ n)       +ℤ (+ m)       = + (n +ℕ+ m)
(+ (suc n)) +ℤ (- (suc m)) = n -ℕ2ℤ m
(- n)       +ℤ (- m)       = - (n +ℕ+ m)
(- (suc n)) +ℤ (+ (suc m)) = m -ℕ2ℤ n

_*ℤ_ : ℤ → ℤ → ℤ
z           *ℤ zero               = zero
zero        *ℤ z                  = zero
(+ (suc n)) *ℤ (+ (suc m)) = + suc (n * m + n + m)
(+ (suc n)) *ℤ (- (suc m)) = - suc (n * m + n + m)
(- (suc n)) *ℤ (+ (suc m)) = - suc (n * m + n + m)
(- (suc n)) *ℤ (- (suc m)) = + suc (n * m + n + m)

_-ℤ_ : ℤ → ℤ → ℤ
z -ℤ z' = z +ℤ (minusℤ z')

_*ℤℕ+_ : ℤ → ℕ+ → ℤ
z *ℤℕ+ n = z *ℤ (+ n)

-- temporiliy only for easy

_*m_ : ℤ → ℕ+ → ℤ
z *m z' = z *ℤℕ+ z'

0ℤ  : ℤ
0ℤ  = zero

1ℤ  : ℤ
1ℤ  = + 1ℕ+

2ℤ  : ℤ
2ℤ  = + 2ℕ+

-1ℤ  : ℤ
-1ℤ  = - 1ℕ+

-2ℤ  : ℤ
-2ℤ  = - 2ℕ+```