[Agda] Integer lemmata

[Sergei Meshveliani]

People,

this is on  Standard library lib-0.7.

I need to use 15-20 trivial lemmata for  Integer,  like these:

       x * (+ 0) ≡ + 0
       x * (- y) ≡ - (x * y)

For this, I use  Data.Integer.Properties.commutativeRing,
and still write the code shown below.

I suspect that I write for this too much code of my own.
Consider, for example,  `-*' below.  
Can this be simplified? (may be, by taking something from library). 

Thanks,

------
Sergei


-------------------------------------------------------------------------------
open import Data.Integer as Int using (ℤ; module ℤ; sign; _◃_; ∣_∣)
open import Data.Integer.Properties as IntProp using (commutativeRing)
...
natCommSemir = NatProp.commutativeSemiring
open CommutativeSemiring natCommSemir using () 
                                 renaming (*-comm to *comm-nat)
intCommRing = IntProp.commutativeRing
open CommRing' intCommRing
               using (+-isAbelianGroup; _+_; -_; _-_; _*_; +-assoc;
                      +-comm; *-assoc; *-comm; distrib; *-identity)

open IsAbelianGroup +-isAbelianGroup using ()
                      renaming (identity to zero; inverse to opposite)
open ℤ

+0≢+m' : ∀ {m} → + 0 ≢ + (sucN m)
+0≢+m' ()

+m≢- : {m n : ℕ} → (+ m) ≢ -[1+ n ]
+m≢- ()

0+ : (x : ℤ) → (+ 0) + x ≡ x
0+ = proj₁ zero

+0 : (x : ℤ) → x + (+ 0) ≡ x
+0 = proj₂ zero

x+-x : (x : ℤ) → x + (- x) ≡ (+ 0)
x+-x = proj₂ opposite

-x+x : (x : ℤ) → (- x) + x ≡ (+ 0)
-x+x = proj₁ opposite

*1 : (x : ℤ) → x * (+ 1) ≡ x
*1 = proj₂ *-identity

*0 : (x : ℤ) → x * (+ 0) ≡ + 0   -- *** where to take it from? 
*0 x =
       ≡begin  x * (+ 0)          ≡[ PE.refl ]
               sg ◃ (∣ x ∣ *n 0)  ≡[ PE.cong (_◃_ sg) $ Nat2.*0 ∣ x ∣ ]
               sg ◃ 0             ≡[ PE.refl ]
               + 0
       ≡end

0* :  (x : ℤ) → (+ 0) * x ≡ + 0
0* x =  PE.trans (*-comm (+ 0) x) $ *0 x

+◃ : (m : ℕ) → (Sign.+ ◃ m) ≡ + m
+◃ 0        = PE.refl
+◃ (sucN _) = PE.refl

-◃ : (m : ℕ) → (Sign.- ◃ m) ≡ - (+ m)
-◃ 0        = PE.refl
-◃ (sucN _) = PE.refl

+m*+n= : (m n : ℕ) → (+ m) * (+ n) ≡ + (m *n n) 
+m*+n= m n =
             ≡begin  (+ m) * (+ n)       ≡[ PE.refl ]
                     Sign.+ ◃ (m *n n)   ≡[ +◃ (m *n n) ]
                     + (m *n n)
             ≡end
--
-- ** where to take them?
-- 
+m*-n'= :  (m n : ℕ) →  (+ m) * -[1+ n ] ≡ - (+ (m *n sucN n))
+m*-n'= m n =
             ≡begin  (+ m) * -[1+ n ]        ≡[ PE.refl ]
                     Sign.- ◃ (m *n sucN n)  ≡[ -◃ (m *n sucN n) ]
                     - (+ (m *n sucN n))
             ≡end

negneg : (x : ℤ) → - (- x) ≡ x   -- **
negneg (+ 0)      = PE.refl
negneg (+ sucN _) = PE.refl
negneg -[1+ _ ]   = PE.refl


-* : (x y : ℤ) → (- x) * y ≡ - (x * y)

-* (+ 0)      _     =  PE.refl
-* x          (+ 0) =  
                ≡begin (- x) * (+ 0)    ≡[ *0 (- x) ]
                       (+ 0)            ≡[ PE.refl ]
                       - (+ 0)          ≡[ PE.cong -_ $ PE.sym $ *0 x ]
                              - (x * (+ 0))
                ≡end
-* (+ sucN _) (+ sucN _) =  PE.refl
-* (+ sucN _) -[1+ _ ]   =  PE.refl
-* -[1+ _ ]   (+ sucN _) =  PE.refl
-* -[1+ _ ]   -[1+ _ ]   =  PE.refl


*- : (x y : ℤ) → x * (- y) ≡ - (x * y)
*- x y =
         ≡begin  x * (- y)    ≡[ *-comm x (- y) ]
                 (- y) * x    ≡[ -* y x ]
                 - (y * x)    ≡[ PE.cong -_ $ *-comm y x ]
                 - (x * y)
         ≡end

-*- : (x y : ℤ) → (- x) * (- y) ≡ x * y
-*- x y =
          ≡begin  (- x) * (- y)   ≡[ -* x (- y) ]
                  - (x * (- y))   ≡[ PE.cong -_ $ *- x y ]
                  - (- (x * y))   ≡[ negneg _ ]
                  x * y
          ≡end