(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                  Zadd.v                                  *)
(****************************************************************************)

Require Export Arith.
Require Export Nat_complements.
Require Export Lci.
Require Export groups.
Require Export rings.
Require Export Zbase.
Require Export Z_succ_pred.

(* Addition on Z, (Z, +) is a group *)

(*Recursive Definition addZ : Z -> Z -> Z := 
       OZ        y => y
|   (pos O)      y => (succZ y)
|   (pos (S n1)) y => (succZ (addZ (pos n1) y))
|   (neg O)      y => (predZ y)
|   (neg (S n1)) y => (predZ (addZ (neg n1) y)).*)


(* this definition introduces unnecessary names *)


Fixpoint addpos (x2 : Z) (n : nat) {struct n} : Z :=
  match n with
  | O => succZ x2
  | S n0 => succZ (addpos x2 n0)
  end.

Fixpoint addneg (x2 : Z) (n : nat) {struct n} : Z :=
  match n with
  | O => predZ x2
  | S n0 => predZ (addneg x2 n0)
  end.

Definition addZ (x1 x2 : Z) :=
  match x1 with
  | OZ => x2
  | pos n => addpos x2 n
  | neg n => addneg x2 n
  end.


Lemma addZ_eq1 : forall y : Z, addZ OZ y = y.
Proof.
(* Goal: forall (n1 : nat) (y : Z), @eq Z (addZ (neg (S n1)) y) (predZ (addZ (neg n1) y)) *)
auto with arith.
Qed.

Lemma addZ_eq2 : forall y : Z, addZ (pos 0) y = succZ y.
Proof.
(* Goal: forall (n1 : nat) (y : Z), @eq Z (addZ (neg (S n1)) y) (predZ (addZ (neg n1) y)) *)
auto with arith.
Qed.

Lemma addZ_eq3 :
 forall (n1 : nat) (y : Z), addZ (pos (S n1)) y = succZ (addZ (pos n1) y).
Proof.
(* Goal: forall (n1 : nat) (y : Z), @eq Z (addZ (neg (S n1)) y) (predZ (addZ (neg n1) y)) *)
auto with arith.
Qed.

Lemma addZ_eq4 : forall y : Z, addZ (neg 0) y = predZ y.
Proof.
(* Goal: forall (n1 : nat) (y : Z), @eq Z (addZ (neg (S n1)) y) (predZ (addZ (neg n1) y)) *)
auto with arith.
Qed.

Lemma addZ_eq5 :
 forall (n1 : nat) (y : Z), addZ (neg (S n1)) y = predZ (addZ (neg n1) y).
Proof.
(* Goal: forall (n1 : nat) (y : Z), @eq Z (addZ (neg (S n1)) y) (predZ (addZ (neg n1) y)) *)
auto with arith.
Qed.



(***************)
Lemma succ_addZ_l : forall x y : Z, addZ (succZ x) y = succZ (addZ x y).

(* Goal: forall x y : Z, @eq Z (addZ x (predZ y)) (predZ (addZ x y)) *)
intros; elim x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos n *)
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
trivial.
(* neg n *)
(* Goal: forall n : nat, @eq Z (addZ (predZ (pos n)) y) (predZ (addZ (pos n) y)) *)
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
simple destruct n.
(* neg O *)
simpl in |- *; symmetry  in |- *; exact (succ_predZ y). 
(* neg (S n0) *)
intros; symmetry  in |- *; rewrite addZ_eq5.
(* Goal: @eq Z (succZ (predZ (addZ (neg n0) y))) (addZ (succZ (neg (S n0))) y) *)
apply succ_predZ.
Qed.

(***************)
Lemma pred_addZ_l : forall x y : Z, addZ (predZ x) y = predZ (addZ x y).

(* Goal: forall x y : Z, @eq Z (addZ x (predZ y)) (predZ (addZ x y)) *)
intros; elim x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos n *)
(* Goal: forall n : nat, @eq Z (addZ (predZ (pos n)) y) (predZ (addZ (pos n) y)) *)
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
simple destruct n.
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
simpl in |- *; rewrite pred_succZ; trivial.
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
intros; rewrite addZ_eq3; rewrite pred_succZ; trivial.
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
trivial.
Qed.

(**********************)
Lemma tech_add_pos_succZ :
 forall (x : nat) (y : Z), addZ (pos (S x)) y = succZ (addZ (pos x) y).
Proof addZ_eq3.

(**********************)
Lemma tech_add_neg_predZ :
 forall (x : nat) (y : Z), addZ (neg (S x)) y = predZ (addZ (neg x) y).
Proof addZ_eq5.

(***************)
Lemma succ_addZ_r : forall x y : Z, addZ x (succZ y) = succZ (addZ x y).

(* Goal: forall x y : Z, @eq Z (addZ x (predZ y)) (predZ (addZ x y)) *)
intros; elim x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos n *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* pos O *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos y0 *)
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
intros.
(* Goal: @eq Z (addZ (pos (S n0)) (addZ y z)) (addZ (addZ (pos (S n0)) y) z) *)
(* Goal: forall n : nat, @eq Z (addZ (neg n) (addZ y z)) (addZ (addZ (neg n) y) z) *)
do 2 rewrite (tech_add_pos_succZ n0).
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
elim H; reflexivity.
(* neg n *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* neg O *)
simpl in |- *; symmetry  in |- *; apply succ_pred_pred_succZ.
(* neg y0 *)
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
intros.
(* Goal: @eq Z (addZ (neg (S n0)) (addZ y z)) (addZ (addZ (neg (S n0)) y) z) *)
do 2 rewrite (tech_add_neg_predZ n0).
(* Goal: @eq Z (predZ (addZ (neg n0) y)) (addZ y (neg (S n0))) *)
rewrite H.
symmetry  in |- *; apply succ_pred_pred_succZ.
Qed.

(***************)
Lemma pred_addZ_r : forall x y : Z, addZ x (predZ y) = predZ (addZ x y).

(* Goal: forall x y : Z, @eq Z (addZ x (predZ y)) (predZ (addZ x y)) *)
intros; elim x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* (pos n) *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* (pos O) *)
(* Goal: @eq Z (addZ (pos O) (predZ y)) (predZ (addZ (pos O) y)) *)
(* Goal: forall (n : nat) (_ : @eq Z (addZ (pos n) (predZ y)) (predZ (addZ (pos n) y))), @eq Z (addZ (pos (S n)) (predZ y)) (predZ (addZ (pos (S n)) y)) *)
(* Goal: forall n : nat, @eq Z (addZ (neg n) (predZ y)) (predZ (addZ (neg n) y)) *)
simpl in |- *; apply succ_pred_pred_succZ.
(* (pos (S y0)) *)
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
intros.
(* Goal: @eq Z (addZ (pos (S n0)) (addZ y z)) (addZ (addZ (pos (S n0)) y) z) *)
(* Goal: forall n : nat, @eq Z (addZ (neg n) (addZ y z)) (addZ (addZ (neg n) y) z) *)
do 2 rewrite (tech_add_pos_succZ n0).
(* Goal: @eq Z (succZ (addZ (pos n0) (predZ y))) (predZ (succZ (addZ (pos n0) y))) *)
(* Goal: forall n : nat, @eq Z (addZ (neg n) (predZ y)) (predZ (addZ (neg n) y)) *)
rewrite H; apply succ_pred_pred_succZ.
(* neg n *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* neg O *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* neg (S y0) *)
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
intros.
(* Goal: @eq Z (addZ (neg (S n0)) (addZ y z)) (addZ (addZ (neg (S n0)) y) z) *)
do 2 rewrite (tech_add_neg_predZ n0).
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
elim H; reflexivity.
Qed.

(***********)
Lemma add_OZ : forall x : Z, addZ x OZ = x.

(* Goal: forall x : Z, @eq Z (addZ x OZ) x *)
simple induction x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos n *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; rewrite tech_add_pos_succZ; rewrite H; reflexivity.
(* neg n *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; rewrite tech_add_neg_predZ; rewrite H; reflexivity.
Qed.

(*****************)
Lemma add_IZ_succZ : forall x : Z, addZ x IZ = succZ x.

(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
intros.
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
cut (succZ OZ = IZ); intros. elim H.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
rewrite (succ_addZ_r x OZ); rewrite (add_OZ x); reflexivity.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
Qed.

(*****************)
Lemma add_mIZ_predZ : forall x : Z, addZ x (neg 0) = predZ x.

(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
intros.
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
cut (predZ OZ = neg 0); intros. elim H.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
rewrite (pred_addZ_r x OZ); rewrite (add_OZ x); reflexivity.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
Qed.

(*************************)
Theorem addZ_commutativity : commutativity Z addZ.

(* Goal: forall x y : Z, @eq Z (addZ x (predZ y)) (predZ (addZ x y)) *)
unfold commutativity in |- *; intros; elim x.
(* OZ *)
simpl in |- *; symmetry  in |- *; exact (add_OZ y).
(* pos n *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* pos O *)
simpl in |- *; symmetry  in |- *; exact (add_IZ_succZ y).
(* pos (S y0) *)
(* Goal: @eq Z (predZ (addZ (neg n0) y)) (addZ y (neg (S n0))) *)
intros; rewrite (tech_add_pos_succZ n0 y). rewrite H.
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
cut (succZ (pos n0) = pos (S n0)); intros. elim H0.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
rewrite (succ_addZ_r y (pos n0)); reflexivity.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* neg n *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* neg O *)
simpl in |- *; symmetry  in |- *; exact (add_mIZ_predZ y).
(* neg (S y0) *)
(* Goal: @eq Z (predZ (addZ (neg n0) y)) (addZ y (neg (S n0))) *)
intros; rewrite (tech_add_neg_predZ n0 y). rewrite H.
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
cut (predZ (neg n0) = neg (S n0)); intros. elim H0.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
rewrite (pred_addZ_r y (neg n0)); reflexivity.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
Qed.

(*************************)
Lemma tech_add_pos_neg_posZ :
 forall n1 n2 : nat, n2 < n1 -> addZ (pos n1) (neg n2) = pos (n1 - S n2).

(* Goal: forall (n1 n2 : nat) (_ : lt n2 n1), @eq Z (addZ (pos n1) (neg n2)) (pos (Init.Nat.sub n1 (S n2))) *)
simple induction n2.
(* O *)
(* Goal: forall _ : lt O n1, @eq Z (addZ (pos n1) (neg O)) (pos (Init.Nat.sub n1 (S O))) *)
(* Goal: forall (n : nat) (_ : forall _ : lt n n1, @eq Z (addZ (pos n1) (neg n)) (pos (Init.Nat.sub n1 (S n)))) (_ : lt (S n) n1), @eq Z (addZ (pos n1) (neg (S n))) (pos (Init.Nat.sub n1 (S (S n)))) *)
intros; elim (addZ_commutativity (neg 0) (pos n1)).
(* Goal: @eq Z (addZ (neg O) (pos n1)) (pos (Init.Nat.sub n1 (S O))) *)
(* Goal: forall (n : nat) (_ : forall _ : lt n n1, @eq Z (addZ (pos n1) (neg n)) (pos (Init.Nat.sub n1 (S n)))) (_ : lt (S n) n1), @eq Z (addZ (pos n1) (neg (S n))) (pos (Init.Nat.sub n1 (S (S n)))) *)
rewrite addZ_eq4.
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
elim minus_n_Sm; trivial.
(* Goal: @eq Z (predZ (pos n1)) (pos (Init.Nat.pred (Init.Nat.sub n1 O))) *)
(* Goal: forall (n : nat) (_ : forall _ : lt n n1, @eq Z (addZ (pos n1) (neg n)) (pos (Init.Nat.sub n1 (S n)))) (_ : lt (S n) n1), @eq Z (addZ (pos n1) (neg (S n))) (pos (Init.Nat.sub n1 (S (S n)))) *)
elim minus_n_O.
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
apply tech_pred_posZ; trivial.
(* S y *)
(* Goal: forall (n : nat) (_ : forall _ : lt n n1, @eq Z (addZ (pos n1) (neg n)) (pos (Init.Nat.sub n1 (S n)))) (_ : lt (S n) n1), @eq Z (addZ (pos n1) (neg (S n))) (pos (Init.Nat.sub n1 (S (S n)))) *)
intros; elim (addZ_commutativity (neg (S n)) (pos n1)).
(* Goal: @eq Z (addZ (neg (S n)) (pos n1)) (pos (Init.Nat.sub n1 (S (S n)))) *)
rewrite tech_add_neg_predZ.
(* Goal: @eq Z (predZ (addZ (neg n) (pos n1))) (pos (Init.Nat.sub n1 (S (S n)))) *)
elim (addZ_commutativity (pos n1) (neg n)).
(* Goal: forall (n1 : nat) (y : Z), @eq Z (addZ (neg (S n1)) y) (predZ (addZ (neg n1) y)) *)
rewrite H; auto with arith.
(* Goal: @eq Z (predZ (pos (Init.Nat.sub n1 (S n)))) (pos (Init.Nat.sub n1 (S (S n)))) *)
elim (minus_n_Sm n1 (S n) H0).
(* Goal: @eq Z (predZ (pos (Init.Nat.sub n1 (S n)))) (pos (Init.Nat.pred (Init.Nat.sub n1 (S n)))) *)
apply tech_pred_posZ.
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
apply lt_minus2; trivial.
Qed.

(*************************)
Theorem addZ_associativity : associativity Z addZ.

(* Goal: forall x y : Z, @eq Z (addZ x (predZ y)) (predZ (addZ x y)) *)
unfold associativity in |- *; intros; elim x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
unfold addZ in |- *; reflexivity.
(* pos n *)
(* Goal: forall n m : nat, @eq Z (addZ (pos n) (pos m)) (pos (S (Init.Nat.add n m))) *)
intros; elim n.
(* pos O *)
simpl in |- *; symmetry  in |- *; exact (succ_addZ_l y z).
(* pos (S y0) *)
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
intros.
(* Goal: @eq Z (addZ (pos (S n0)) (addZ y z)) (addZ (addZ (pos (S n0)) y) z) *)
(* Goal: forall n : nat, @eq Z (addZ (neg n) (addZ y z)) (addZ (addZ (neg n) y) z) *)
do 2 rewrite (tech_add_pos_succZ n0).
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
rewrite (succ_addZ_l (addZ (pos n0) y) z); elim H; reflexivity.
(* neg n *)
(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* neg O *)
simpl in |- *; symmetry  in |- *; exact (pred_addZ_l y z).
(* neg (S n0) *)
(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
intros.
(* Goal: @eq Z (addZ (neg (S n0)) (addZ y z)) (addZ (addZ (neg (S n0)) y) z) *)
do 2 rewrite (tech_add_neg_predZ n0).
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
rewrite (pred_addZ_l (addZ (neg n0) y) z); elim H; reflexivity.
Qed.

(************)
Definition IdZ (x : Z) := True.

(*******************)
Theorem addZ_neutral : neutral Z IdZ addZ OZ.

(* Goal: forall (x : Z) (_ : IdZ x), and (@eq Z (addZ x OZ) x) (@eq Z (addZ OZ x) x) *)
unfold neutral in |- *; intros.
(* Goal: and (neutral Z IdZ addZ OZ) (opposite Z IdZ addZ OZ oppZ) *)
split. exact I.
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros. split. exact (add_OZ x). unfold addZ in |- *; reflexivity.
Qed.

(*************)
Definition oppZ (x : Z) :=
  match x return Z with
  | OZ =>
      (* OZ *)  OZ
      (* pos n *) 
  | pos n => neg n
      (* neg n *) 
  | neg n => pos n
  end.

(*************)
Lemma opp_succZ : forall x : Z, oppZ (succZ x) = predZ (oppZ x).

(* Goal: forall x : Z, @eq Z (oppZ (predZ x)) (succZ (oppZ x)) *)
simple destruct x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos n *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; reflexivity.
(* neg n *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
simple destruct n; intros; reflexivity. 
Qed.

(*************)
Lemma opp_predZ : forall x : Z, oppZ (predZ x) = succZ (oppZ x).

(* Goal: forall x : Z, @eq Z (oppZ (predZ x)) (succZ (oppZ x)) *)
simple destruct x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos n *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
simple destruct n; intros; reflexivity. 
(* neg n *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; reflexivity.
Qed.

(*********************)
Lemma tech_add_pos_negZ : forall n : nat, addZ (pos n) (neg n) = OZ.

(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* O *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* S y *)
(* Goal: forall (n : nat) (_ : @eq Z (addZ (pos n) (neg n)) OZ), @eq Z (addZ (pos (S n)) (neg (S n))) OZ *)
intros; rewrite (tech_add_pos_succZ n0).
(* Goal: @eq Z (succZ (addZ (pos n0) (neg (S n0)))) OZ *)
elim succ_addZ_r; exact H.
Qed.

(*********************)
Lemma tech_add_neg_posZ : forall n : nat, addZ (neg n) (pos n) = OZ.

intros; elim (addZ_commutativity (pos n) (neg n));
 exact (tech_add_pos_negZ n).
Qed.

(*********************)
Lemma tech_add_pos_posZ :
 forall n m : nat, addZ (pos n) (pos m) = pos (S (n + m)).

(* Goal: forall n m : nat, @eq Z (addZ (pos n) (pos m)) (pos (S (Init.Nat.add n m))) *)
intros; elim n.
(* O *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* S n0 *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; rewrite (tech_add_pos_succZ n0 (pos m)); rewrite H; reflexivity.
Qed.

(*********************)
Lemma tech_add_neg_negZ :
 forall n m : nat, addZ (neg n) (neg m) = neg (S (n + m)).

(* Goal: forall n m : nat, @eq Z (addZ (neg n) (neg m)) (neg (S (Init.Nat.add n m))) *)
simple induction n.
(* O *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* S n0 *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; rewrite (tech_add_neg_predZ n0 (neg m)); rewrite H; reflexivity.
Qed.

(********************)
Theorem addZ_opposite : opposite Z IdZ addZ OZ oppZ.

(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
repeat split; trivial.
(* -> *)
(* Goal: @eq Z (addZ (oppZ x) x) OZ *)
case x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos n *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; exact (tech_add_pos_negZ n).
(* neg n *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; exact (tech_add_neg_posZ n).
(* <- *)
(* Goal: @eq Z (addZ (oppZ x) x) OZ *)
case x.
(* OZ *)
(* Goal: @eq Z (addZ (oppZ OZ) OZ) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
reflexivity.
(* pos n *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (pos n)) (pos n)) OZ *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; exact (tech_add_neg_posZ n).
(* neg n *)
(* Goal: forall n : nat, @eq Z (addZ (oppZ (neg n)) (neg n)) OZ *)
intros; exact (tech_add_pos_negZ n).
Qed.

(**************)
Theorem Z_group : is_group Z IdZ addZ OZ oppZ.

(* Goal: and (neutral Z IdZ addZ OZ) (opposite Z IdZ addZ OZ oppZ) *)
split.
(* Goal: forall n : nat, @eq Z (addZ (predZ (neg n)) y) (predZ (addZ (neg n) y)) *)
red in |- *; trivial.
(* Goal: and (neutral Z IdZ addZ OZ) (opposite Z IdZ addZ OZ oppZ) *)
split. exact addZ_associativity.
(* Goal: and (neutral Z IdZ addZ OZ) (opposite Z IdZ addZ OZ oppZ) *)
split. exact addZ_neutral.
(* Goal: opposite Z IdZ addZ OZ oppZ *)
exact addZ_opposite.
Qed.

(********************)
Theorem abs_eq_or_oppZ : forall x : Z, {absZ x = x} + {absZ x = oppZ x}.

(* Goal: forall (n1 : nat) (y : Z), @eq Z (addZ (neg (S n1)) y) (predZ (addZ (neg n1) y)) *)
simple destruct x; auto with arith.
Qed.

(*********************)
Lemma tech_opp_pos_negZ :
 forall n : nat, oppZ (pos n) = neg n /\ oppZ (neg n) = pos n.

(* Goal: forall (n1 : nat) (y : Z), @eq Z (addZ (neg (S n1)) y) (predZ (addZ (neg n1) y)) *)
simple induction n; auto with arith.
Qed.