Require Import quotient.
Require Export integer_defs.
Require Export PlusZ.
Require Export MultZ.
Require Import AC.
Require Import HS.

Section INT.


Open Scope INT_scope.


Axiom plusZ_simpl_l : forall n m p : Z, m = p -> n + m = n + p.

Axiom multZ_simpl_l : forall n m p : Z, m = p -> n * m = n * p.

End INT.

Ltac CZa := intros; ac_of eq plusZ plusZ_sym plusZ_permute; auto.

Ltac AZa := intros; repeat elim plusZ_assoc_l.

Ltac ACZa :=
  intros; repeat elim plusZ_assoc_l; ac_of eq plusZ plusZ_sym plusZ_permute;
   auto.

Ltac HSZa := intros; hs_of eq plusZ plusZ_sym plusZ_permute plusZ_simpl_l.


Ltac CZm := intros; ac_of eq multZ multZ_sym multZ_permute; auto.

Ltac AZm := intros; repeat elim multZ_assoc_l.

Ltac ACZm :=
  intros; repeat elim multZ_assoc_l; ac_of eq multZ multZ_sym multZ_permute;
   auto.

Ltac HSZm := intros; hs_of eq multZ multZ_sym multZ_permute multZ_simpl_l.