module IntegerProp where
 
open import Data.Nat renaming ( _+_ to _+ℕ_ )
open import Data.Integer renaming ( _+_ to _+ℤ_ ; _-_ to _-ℤ_ ; suc to sucℤ )
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Algebra

import Data.Nat.Properties as Nat
private
  module CS = CommutativeSemiring Nat.commutativeSemiring


ℤ+-identity : {x : ℤ} → ((x +ℤ (+ 0)) ≡ x)
ℤ+-identity { -[1+ m ]} = refl 
ℤ+-identity {+ m} = cong (λ x → + x) (CS.+-comm m 0)

ℤ+-comm : {x y : ℤ} → (x +ℤ y ≡ y +ℤ x)
ℤ+-comm {+ m}{+ n} = 
 begin
  (+ m +ℤ + n)
 ≡⟨ refl ⟩
  + (m +ℕ n)
 ≡⟨ cong (λ x → + x) (CS.+-comm m n) ⟩
  + (n +ℕ m)
 ≡⟨ sym refl ⟩
  (+ n +ℤ + m)
 ∎
ℤ+-comm {+ m}{ -[1+ n ]} = 
 begin
  (+ m) +ℤ -[1+ n ]
 ≡⟨ refl ⟩
  m ⊖ suc n
 ≡⟨ sym refl ⟩
  -[1+ n ] +ℤ (+ m)
 ∎
ℤ+-comm { -[1+ n ] }{+ m} =
 begin
  (+ m) +ℤ -[1+ n ]
 ≡⟨ refl ⟩
  m ⊖ suc n
 ≡⟨ sym refl ⟩
  -[1+ n ] +ℤ (+ m)
 ∎
ℤ+-comm { -[1+ m ] }{ -[1+ n ]} =
 begin
  -[1+ m ] +ℤ -[1+ n ]
 ≡⟨ refl ⟩
  -[1+ suc (m +ℕ n)]
 ≡⟨ cong (λ x → -[1+ suc x ]) (CS.+-comm m n) ⟩
  -[1+ suc (n +ℕ m)]
 ≡⟨ sym refl ⟩
  -[1+ n ] +ℤ -[1+ m ]
 ∎