------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to addition of integers
--
-- This module is DEPRECATED. Please use the corresponding properties in
-- Data.Integer.Properties directly.
------------------------------------------------------------------------

module Data.Integer.Addition.Properties where

open import Data.Integer.Properties public
  using
  ( distribˡ-⊖-+-neg
  ; distribʳ-⊖-+-neg
  ; distribˡ-⊖-+-pos
  ; distribʳ-⊖-+-pos
  )
  renaming
  ( +-comm                  to comm
  ; +-identityˡ             to identityˡ
  ; +-identityʳ             to identityʳ
  ; +-assoc                 to assoc
  ; +-isSemigroup           to isSemigroup
  ; +-0-isCommutativeMonoid to isCommutativeMonoid
  ; +-0-commutativeMonoid   to commutativeMonoid
  )