(* 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                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 Zmult.v                                  *)
(****************************************************************************)
Require Export Lci.
Require Export misc.
Require Export Arith.
Require Export Nat_complements.
Require Export groups.
Require Export rings.
Require Export Zbase.
Require Export Z_succ_pred.
Require Export Zadd.

(* Multiplication on Z, (Z, +, *, 0, 1) is a unitary commutative ring *)

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


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

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

Definition multZ (x1 x2 : Z) :=
  match x1 with
  | OZ => OZ
  | pos n => multpos x2 n
  | neg n => multneg x2 n
  end.


Lemma multZ_eq1 : forall n : Z, multZ OZ n = OZ.
Proof.
(* Goal: forall (n1 : nat) (n : Z), @eq Z (multZ (neg (S n1)) n) (addZ (multZ (neg n1) n) (oppZ n)) *)
 auto.
Qed.

Lemma multZ_eq2 : forall n : Z, multZ (pos 0) n = n.
Proof.
(* Goal: forall (n1 : nat) (n : Z), @eq Z (multZ (neg (S n1)) n) (addZ (multZ (neg n1) n) (oppZ n)) *)
 auto.
Qed.

Lemma multZ_eq3 :
 forall (n1 : nat) (n : Z), multZ (pos (S n1)) n = addZ (multZ (pos n1) n) n.
Proof.
(* Goal: forall (n1 : nat) (n : Z), @eq Z (multZ (neg (S n1)) n) (addZ (multZ (neg n1) n) (oppZ n)) *)
 auto.
Qed.

Lemma multZ_eq4 : forall n : Z, multZ (neg 0) n = oppZ n.
Proof.
(* Goal: forall (n1 : nat) (n : Z), @eq Z (multZ (neg (S n1)) n) (addZ (multZ (neg n1) n) (oppZ n)) *)
 auto.
Qed.

Lemma multZ_eq5 :
 forall (n1 : nat) (n : Z),
 multZ (neg (S n1)) n = addZ (multZ (neg n1) n) (oppZ n).
Proof.
(* Goal: forall (n1 : nat) (n : Z), @eq Z (multZ (neg (S n1)) n) (addZ (multZ (neg n1) n) (oppZ n)) *)
 auto.
Qed.

(*******************)
Lemma tech_mult_posZ :
 forall (x : nat) (y : Z), multZ (pos (S x)) y = addZ (multZ (pos x) y) y.

Proof multZ_eq3.

(*******************)
Lemma tech_mult_negZ :
 forall (x : nat) (y : Z),
 multZ (neg (S x)) y = addZ (multZ (neg x) y) (oppZ y).

Proof multZ_eq5.

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

(* Goal: forall x y : Z, @eq Z (multZ x (predZ y)) (addZ (multZ x y) (oppZ x)) *)
intros; elim x.
(* OZ *)
(* Goal: @eq Z (multZ (neg O) (pos m)) (neg (Init.Nat.add (Init.Nat.mul O m) (Init.Nat.add O m))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m)))), @eq Z (multZ (neg (S n)) (pos m)) (neg (Init.Nat.add (Init.Nat.mul (S n) m) (Init.Nat.add (S n) m))) *)
simpl in |- *; reflexivity.
(* pos n *)
(* Goal: @eq Z (multZ (neg O) (pos m)) (neg (Init.Nat.add (Init.Nat.mul O m) (Init.Nat.add O m))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m)))), @eq Z (multZ (neg (S n)) (pos m)) (neg (Init.Nat.add (Init.Nat.mul (S n) m) (Init.Nat.add (S n) m))) *)
intros; simpl in |- *; reflexivity.
(* neg n *)
(* Goal: forall n m : nat, @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m))) *)
intros; elim n.
(* neg O *)
simpl in |- *; symmetry  in |- *. 
(* Goal: @eq Z (multZ (pos n0) y) (addZ (multZ (pos n0) y) (addZ y (oppZ y))) *)
(* Goal: forall n : nat, @eq Z (multZ (predZ (neg n)) y) (addZ (multZ (neg n) y) (oppZ y)) *)
elim (addZ_opposite y I); intros. elim H0; intros; elim H2; intros; exact H4.
(* neg (S n0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (succZ (neg n)) y) (addZ (multZ (neg n) y) y)), @eq Z (multZ (succZ (neg (S n))) y) (addZ (multZ (neg (S n)) y) y) *)
intros; unfold succZ in |- *; rewrite (tech_mult_negZ n0 y).
(* Goal: @eq Z (multZ (neg n0) y) (addZ (addZ (multZ (neg n0) y) (oppZ y)) y) *)
elim (addZ_associativity (multZ (neg n0) y) (oppZ y) y).
(* Goal: @eq Z (multZ (pos n0) y) (addZ (multZ (pos n0) y) (addZ y (oppZ y))) *)
(* Goal: forall n : nat, @eq Z (multZ (predZ (neg n)) y) (addZ (multZ (neg n) y) (oppZ y)) *)
elim (addZ_opposite y I); intros. elim H1; intros; elim H3; intros. rewrite H5.
symmetry  in |- *; exact (add_OZ (multZ (neg n0) y)).
Qed.

(*****************)
Lemma mult_predZ_l :
 forall x y : Z, multZ (predZ x) y = addZ (multZ x y) (oppZ y).

Proof.
(* Goal: forall x y : Z, @eq Z (multZ x (predZ y)) (addZ (multZ x y) (oppZ x)) *)
intros; elim x.
(* OZ *)
(* Goal: @eq Z (multZ (neg O) (pos m)) (neg (Init.Nat.add (Init.Nat.mul O m) (Init.Nat.add O m))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m)))), @eq Z (multZ (neg (S n)) (pos m)) (neg (Init.Nat.add (Init.Nat.mul (S n) m) (Init.Nat.add (S n) m))) *)
simpl in |- *; reflexivity.
(* pos n *)
(* Goal: forall n m : nat, @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m))) *)
intros; elim n.
(* pos O *)
simpl in |- *; symmetry  in |- *.
(* Goal: @eq Z (multZ (pos n0) y) (addZ (multZ (pos n0) y) (addZ y (oppZ y))) *)
(* Goal: forall n : nat, @eq Z (multZ (predZ (neg n)) y) (addZ (multZ (neg n) y) (oppZ y)) *)
elim (addZ_opposite y I); intros. elim H0; intros; elim H2; intros; exact H3.
(* pos (S n0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (predZ (pos n)) y) (addZ (multZ (pos n) y) (oppZ y))), @eq Z (multZ (predZ (pos (S n))) y) (addZ (multZ (pos (S n)) y) (oppZ y)) *)
(* Goal: forall n : nat, @eq Z (multZ (predZ (neg n)) y) (addZ (multZ (neg n) y) (oppZ y)) *)
intros; unfold predZ in |- *; rewrite (tech_mult_posZ n0 y).
(* Goal: @eq Z (multZ (pos n0) y) (addZ (addZ (multZ (pos n0) y) y) (oppZ y)) *)
(* Goal: forall n : nat, @eq Z (multZ (predZ (neg n)) y) (addZ (multZ (neg n) y) (oppZ y)) *)
elim (addZ_associativity (multZ (pos n0) y) y (oppZ y)).
(* Goal: @eq Z (multZ (pos n0) y) (addZ (multZ (pos n0) y) (addZ y (oppZ y))) *)
(* Goal: forall n : nat, @eq Z (multZ (predZ (neg n)) y) (addZ (multZ (neg n) y) (oppZ y)) *)
elim (addZ_opposite y I); intros. elim H1; intros; elim H3; intros; rewrite H4.
(* Goal: @eq Z (multZ (pos n0) y) (addZ (multZ (pos n0) y) OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (predZ (neg n)) y) (addZ (multZ (neg n) y) (oppZ y)) *)
rewrite (add_OZ (multZ (pos n0) y)); reflexivity.
(* neg n *)
(* Goal: forall n : nat, @eq Z (multZ (predZ (neg n)) y) (addZ (multZ (neg n) y) (oppZ y)) *)
intros; reflexivity.
Qed.

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

(* Goal: forall x y : Z, @eq Z (multZ x (predZ y)) (addZ (multZ x y) (oppZ x)) *)
intros; elim x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
symmetry  in |- *; exact (add_IZ_succZ y).
(* pos (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) (multZ y z)) (multZ (multZ (pos n) y) z)), @eq Z (multZ (pos (S n)) (multZ y z)) (multZ (multZ (pos (S n)) y) z) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (multZ y z)) (multZ (multZ (neg n) y) z) *)
intros y0 H; do 2 rewrite (tech_mult_posZ y0).
(* Goal: @eq Z (addZ (multZ (pos y0) (succZ y)) (succZ y)) (addZ (addZ (multZ (pos y0) y) y) (pos (S y0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (succZ y)) (addZ (multZ (neg n) y) (neg n)) *)
rewrite H; elim (addZ_commutativity (pos y0) (multZ (pos y0) y)).
(* Goal: @eq Z (addZ (addZ (pos y0) (multZ (pos y0) y)) (succZ y)) (addZ (addZ (multZ (pos y0) y) y) (pos (S y0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (succZ y)) (addZ (multZ (neg n) y) (neg n)) *)
elim (addZ_associativity (pos y0) (multZ (pos y0) y) (succZ y)).
(* Goal: @eq Z (addZ (pos y0) (addZ (multZ (pos y0) y) (succZ y))) (addZ (addZ (multZ (pos y0) y) y) (pos (S y0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (succZ y)) (addZ (multZ (neg n) y) (neg n)) *)
elim (addZ_commutativity (addZ (multZ (pos y0) y) (succZ y)) (pos y0)).
(* Goal: @eq Z (addZ (addZ (multZ (pos y0) y) (succZ y)) (pos y0)) (addZ (addZ (multZ (pos y0) y) y) (pos (S y0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (succZ y)) (addZ (multZ (neg n) y) (neg n)) *)
rewrite (succ_addZ_r (multZ (pos y0) y) y).
(* Goal: @eq Z (addZ (succZ (addZ (multZ (pos y0) y) y)) (pos y0)) (addZ (addZ (multZ (pos y0) y) y) (pos (S y0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (succZ y)) (addZ (multZ (neg n) y) (neg n)) *)
rewrite (succ_addZ_l (addZ (multZ (pos y0) y) y) (pos y0)).
(* Goal: @eq Z (succZ (addZ (addZ (multZ (pos y0) y) y) (pos y0))) (addZ (addZ (multZ (pos y0) y) y) (pos (S y0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (succZ y)) (addZ (multZ (neg n) y) (neg n)) *)
elim (succ_addZ_r (addZ (multZ (pos y0) y) y) (pos y0)).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* neg n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* neg O *)
(* Goal: @eq Z (multZ (neg O) (succZ y)) (addZ (multZ (neg O) y) (neg O)) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (succZ y)) (addZ (multZ (neg n) y) (neg n))), @eq Z (multZ (neg (S n)) (succZ y)) (addZ (multZ (neg (S n)) y) (neg (S n))) *)
simpl in |- *; rewrite (add_mIZ_predZ (oppZ y)); exact (opp_succZ y).
(* neg (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (multZ y z)) (multZ (multZ (neg n) y) z)), @eq Z (multZ (neg (S n)) (multZ y z)) (multZ (multZ (neg (S n)) y) z) *)
intros y0 H; do 2 rewrite (tech_mult_negZ y0).
(* Goal: @eq Z (addZ (multZ (neg y0) (succZ y)) (oppZ (succZ y))) (addZ (addZ (multZ (neg y0) y) (oppZ y)) (neg (S y0))) *)
elim H; elim (addZ_commutativity (oppZ y) (multZ (neg y0) y)).
(* Goal: @eq Z (addZ (multZ (neg y0) (succZ y)) (oppZ (succZ y))) (addZ (addZ (oppZ y) (multZ (neg y0) y)) (neg (S y0))) *)
elim (addZ_associativity (oppZ y) (multZ (neg y0) y) (neg (S y0))).
(* Goal: @eq Z (addZ (multZ (neg y0) (succZ y)) (oppZ (succZ y))) (addZ (oppZ y) (addZ (multZ (neg y0) y) (neg (S y0)))) *)
elim (addZ_commutativity (addZ (multZ (neg y0) y) (neg (S y0))) (oppZ y)).
(* Goal: @eq Z (addZ (multZ (neg y0) (succZ y)) (oppZ (succZ y))) (addZ (addZ (multZ (neg y0) y) (neg (S y0))) (oppZ y)) *)
rewrite (opp_succZ y). 
(* Goal: @eq Z (addZ (multZ (neg y0) (succZ y)) (predZ (oppZ y))) (addZ (addZ (multZ (neg y0) y) (neg (S y0))) (oppZ y)) *)
rewrite (pred_addZ_r (multZ (neg y0) (succZ y)) (oppZ y)).
(* Goal: @eq Z (predZ (addZ (multZ (neg y0) (succZ y)) (oppZ y))) (addZ (addZ (multZ (neg y0) y) (neg (S y0))) (oppZ y)) *)
rewrite H; elim (pred_addZ_l (addZ (multZ (neg y0) y) (neg y0)) (oppZ y)).
elim (pred_addZ_r (multZ (neg y0) y) (neg y0)); unfold predZ in |- *;
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
 reflexivity.
Qed.

(*****************)
Lemma mult_predZ_r :
 forall x y : Z, multZ x (predZ y) = addZ (multZ x y) (oppZ x).

(* Goal: forall x y : Z, @eq Z (multZ x (predZ y)) (addZ (multZ x y) (oppZ x)) *)
intros; elim x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
simpl in |- *; symmetry  in |- *; exact (add_mIZ_predZ y).
(* pos (S n0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) (predZ y)) (addZ (multZ (pos n) y) (oppZ (pos n)))), @eq Z (multZ (pos (S n)) (predZ y)) (addZ (multZ (pos (S n)) y) (oppZ (pos (S n)))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n))) *)
intros n0 H; unfold oppZ in |- *; do 2 rewrite (tech_mult_posZ n0).
(* Goal: @eq Z (addZ (multZ (pos n0) (predZ y)) (predZ y)) (addZ (addZ (multZ (pos n0) y) y) (neg (S n0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n))) *)
rewrite (pred_addZ_r (multZ (pos n0) (predZ y)) y).
(* Goal: @eq Z (predZ (addZ (multZ (pos n0) (predZ y)) y)) (addZ (addZ (multZ (pos n0) y) y) (neg (S n0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n))) *)
elim (pred_addZ_l (multZ (pos n0) (predZ y)) y).
(* Goal: @eq Z (addZ (predZ (multZ (pos n0) (predZ y))) y) (addZ (addZ (multZ (pos n0) y) y) (neg (S n0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n))) *)
elim (addZ_commutativity y (multZ (pos n0) y)).
(* Goal: @eq Z (addZ (predZ (multZ (pos n0) (predZ y))) y) (addZ (addZ y (multZ (pos n0) y)) (neg (S n0))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n))) *)
elim (addZ_associativity y (multZ (pos n0) y) (neg (S n0))).
(* Goal: @eq Z (addZ (predZ (multZ (pos n0) (predZ y))) y) (addZ y (addZ (multZ (pos n0) y) (neg (S n0)))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n))) *)
elim (addZ_commutativity (addZ (multZ (pos n0) y) (neg (S n0))) y).
(* Goal: @eq Z (addZ (predZ (multZ (pos n0) (predZ y))) y) (addZ (addZ (multZ (pos n0) y) (neg (S n0))) y) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n))) *)
rewrite H; elim (pred_addZ_r (multZ (pos n0) y) (oppZ (pos n0))).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* neg n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* neg O *)
(* Goal: @eq Z (multZ (neg O) (predZ y)) (addZ (multZ (neg O) y) (oppZ (neg O))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n)))), @eq Z (multZ (neg (S n)) (predZ y)) (addZ (multZ (neg (S n)) y) (oppZ (neg (S n)))) *)
simpl in |- *.
(* Goal: forall (n1 : nat) (n : Z), @eq Z (multZ (neg (S n1)) n) (addZ (multZ (neg n1) n) (oppZ n)) *)
replace (pos 0) with IZ; auto.
(* Goal: @eq Z (oppZ (predZ y)) (addZ (oppZ y) IZ) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n)))), @eq Z (multZ (neg (S n)) (predZ y)) (addZ (multZ (neg (S n)) y) (oppZ (neg (S n)))) *)
rewrite (add_IZ_succZ (oppZ y)).
(* Goal: @eq Z (oppZ (predZ y)) (succZ (oppZ y)) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n)))), @eq Z (multZ (neg (S n)) (predZ y)) (addZ (multZ (neg (S n)) y) (oppZ (neg (S n)))) *)
exact (opp_predZ y).
(* neg (S n0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n)))), @eq Z (multZ (neg (S n)) (predZ y)) (addZ (multZ (neg (S n)) y) (oppZ (neg (S n)))) *)
intros n0 H; do 2 rewrite (tech_mult_negZ n0).
(* Goal: @eq Z (addZ (multZ (neg n0) (predZ y)) (oppZ (predZ y))) (addZ (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg (S n0)))) *)
rewrite H; rewrite (opp_predZ y).
(* Goal: @eq Z (addZ (addZ (multZ (neg n0) y) (oppZ (neg n0))) (succZ (oppZ y))) (addZ (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg (S n0)))) *)
elim (addZ_commutativity (oppZ (neg n0)) (multZ (neg n0) y)).
(* Goal: @eq Z (addZ (addZ (oppZ (neg n0)) (multZ (neg n0) y)) (succZ (oppZ y))) (addZ (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg (S n0)))) *)
elim (addZ_associativity (oppZ (neg n0)) (multZ (neg n0) y) (succZ (oppZ y))).
elim
 (addZ_commutativity (addZ (multZ (neg n0) y) (succZ (oppZ y)))
    (oppZ (neg n0))).
(* Goal: @eq Z (addZ (addZ (multZ (neg n0) y) (succZ (oppZ y))) (oppZ (neg n0))) (addZ (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg (S n0)))) *)
rewrite (succ_addZ_r (multZ (neg n0) y) (oppZ y)).
(* Goal: @eq Z (addZ (succZ (addZ (multZ (neg n0) y) (oppZ y))) (oppZ (neg n0))) (addZ (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg (S n0)))) *)
rewrite (succ_addZ_l (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg n0))).
(* Goal: @eq Z (succZ (addZ (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg n0)))) (addZ (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg (S n0)))) *)
elim (succ_addZ_r (addZ (multZ (neg n0) y) (oppZ y)) (oppZ (neg n0))).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
Qed.

(************)
Lemma mult_OZ : forall x : Z, multZ x OZ = OZ.

(* Goal: forall x : Z, @eq Z (multZ x (sgnZ x)) (absZ x) *)
simple destruct x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos (S y) *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
intros y H; rewrite (tech_mult_posZ y OZ); rewrite H; reflexivity.
(* neg n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* neg O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* neg (S y) *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
intros y H; rewrite (tech_mult_negZ y OZ); rewrite H; reflexivity.
Qed.

(************)
Lemma mult_IZ : forall x : Z, multZ x IZ = x.

(* Goal: forall x : Z, @eq Z (multZ x (sgnZ x)) (absZ x) *)
simple destruct x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos (S y) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) IZ) (pos n)), @eq Z (multZ (pos (S n)) IZ) (pos (S n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) IZ) (neg n) *)
intros y H; rewrite (tech_mult_posZ y IZ); rewrite H. 
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
rewrite (add_IZ_succZ (pos y)); reflexivity.
(* neg n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* neg O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* neg (S y) *)
intros y H; rewrite (tech_mult_negZ y IZ); rewrite H; unfold IZ in |- *;
 unfold oppZ in |- *. 
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
rewrite (add_mIZ_predZ (neg y)); reflexivity.
Qed.

(*************)
Lemma mult_mIZ : forall x : Z, multZ x (neg 0) = oppZ x.

(* Goal: forall x : Z, @eq Z (multZ x (sgnZ x)) (absZ x) *)
simple destruct x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos (S y) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) (neg O)) (oppZ (pos n))), @eq Z (multZ (pos (S n)) (neg O)) (oppZ (pos (S n))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (neg O)) (oppZ (neg n)) *)
intros y H; rewrite (tech_mult_posZ y (neg 0)); rewrite H. 
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
rewrite (add_mIZ_predZ (oppZ (pos y))); reflexivity.
(* neg n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* neg O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* neg (S y) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (neg O)) (oppZ (neg n))), @eq Z (multZ (neg (S n)) (neg O)) (oppZ (neg (S n))) *)
intros y H; rewrite (tech_mult_negZ y (neg 0)); rewrite H.
elim
 (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity (neg y) (neg 0) I I).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
rewrite (add_mIZ_predZ (neg y)); reflexivity.
Qed.

(**************************)
Theorem multZ_commutativity : commutativity Z multZ.

(* Goal: forall x y : Z, @eq Z (multZ x (predZ y)) (addZ (multZ x y) (oppZ x)) *)
unfold commutativity in |- *; intros; elim x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
rewrite (mult_OZ y); unfold multZ in |- *; reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
simpl in |- *; symmetry  in |- *; exact (mult_IZ y).
(* pos (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) y) (multZ y (pos n))), @eq Z (multZ (pos (S n)) y) (multZ y (pos (S n))) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) y) (multZ y (neg n)) *)
intros y0 H; rewrite (tech_mult_posZ y0 y); rewrite H. 
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (mult_succZ_r y (pos y0)); unfold succZ in |- *; reflexivity.
(* neg n *)
(* Goal: forall n m : nat, @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m))) *)
intros; elim n.
(* neg O *)
simpl in |- *; symmetry  in |- *; exact (mult_mIZ y).
(* neg (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) y) (multZ y (neg n))), @eq Z (multZ (neg (S n)) y) (multZ y (neg (S n))) *)
intros y0 H; rewrite (tech_mult_negZ y0 y); rewrite H. 
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (mult_predZ_r y (neg y0)); unfold predZ in |- *; reflexivity.
Qed.

(********************)
Theorem multZ_neutral : neutral Z IdZ multZ IZ.

(* Goal: neutral Z IdZ multZ IZ *)
unfold neutral in |- *.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split. exact I.
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros. 
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split.
(* -> *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (multZ_commutativity IZ x); reflexivity.
(* <- *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
Qed.

(******************************)
Theorem mult_add_distributivity : distributivity Z addZ multZ.

(* Goal: distributivity Z addZ multZ *)
unfold distributivity in |- *; intros; case x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
split; reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split.
(* Goal: @eq Z (multZ (addZ (pos O) y) z) (addZ (multZ (pos O) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (pos O) (addZ y z)) (addZ (multZ (pos O) y) (multZ (pos O) z)) *)
(* Goal: forall (n : nat) (_ : and (@eq Z (multZ (addZ (pos n) y) z) (addZ (multZ (pos n) z) (multZ y z))) (@eq Z (multZ (pos n) (addZ y z)) (addZ (multZ (pos n) y) (multZ (pos n) z)))), and (@eq Z (multZ (addZ (pos (S n)) y) z) (addZ (multZ (pos (S n)) z) (multZ y z))) (@eq Z (multZ (pos (S n)) (addZ y z)) (addZ (multZ (pos (S n)) y) (multZ (pos (S n)) z))) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
rewrite addZ_eq2; rewrite multZ_eq2.
(* Goal: @eq Z (multZ (succZ y) z) (addZ z (multZ y z)) *)
(* Goal: @eq Z (multZ (pos O) (addZ y z)) (addZ (multZ (pos O) y) (multZ (pos O) z)) *)
(* Goal: forall (n : nat) (_ : and (@eq Z (multZ (addZ (pos n) y) z) (addZ (multZ (pos n) z) (multZ y z))) (@eq Z (multZ (pos n) (addZ y z)) (addZ (multZ (pos n) y) (multZ (pos n) z)))), and (@eq Z (multZ (addZ (pos (S n)) y) z) (addZ (multZ (pos (S n)) z) (multZ y z))) (@eq Z (multZ (pos (S n)) (addZ y z)) (addZ (multZ (pos (S n)) y) (multZ (pos (S n)) z))) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
rewrite (mult_succZ_l y z); exact (addZ_commutativity (multZ y z) z). 
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos (S y0) *)
(* Goal: forall (n : nat) (_ : and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z)))), and (@eq Z (multZ (addZ (neg (S n)) y) z) (addZ (multZ (neg (S n)) z) (multZ y z))) (@eq Z (multZ (neg (S n)) (addZ y z)) (addZ (multZ (neg (S n)) y) (multZ (neg (S n)) z))) *)
intros y0 H.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
elim H; intros; split.
(* Goal: @eq Z (multZ (addZ (pos (S y0)) y) z) (addZ (multZ (pos (S y0)) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (pos (S y0)) (addZ y z)) (addZ (multZ (pos (S y0)) y) (multZ (pos (S y0)) z)) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
rewrite addZ_eq3; rewrite multZ_eq3.
(* Goal: @eq Z (multZ (succZ (addZ (pos y0) y)) z) (addZ (addZ (multZ (pos y0) z) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (pos (S y0)) (addZ y z)) (addZ (multZ (pos (S y0)) y) (multZ (pos (S y0)) z)) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
rewrite mult_succZ_l; rewrite H0.
(* Goal: @eq Z (addZ (addZ (multZ (pos y0) z) (multZ y z)) z) (addZ (addZ (multZ (pos y0) z) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (pos (S y0)) (addZ y z)) (addZ (multZ (pos (S y0)) y) (multZ (pos (S y0)) z)) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
elim (addZ_associativity (multZ (pos y0) z) (multZ y z) z).
(* Goal: @eq Z (addZ (multZ (pos y0) z) (addZ (multZ y z) z)) (addZ (addZ (multZ (pos y0) z) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (pos (S y0)) (addZ y z)) (addZ (multZ (pos (S y0)) y) (multZ (pos (S y0)) z)) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
elim (addZ_commutativity z (multZ y z)).
(* Goal: @eq Z (addZ (multZ (pos y0) z) (addZ z (multZ y z))) (addZ (addZ (multZ (pos y0) z) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (pos (S y0)) (addZ y z)) (addZ (multZ (pos (S y0)) y) (multZ (pos (S y0)) z)) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
apply addZ_associativity.
(* Goal: @eq Z (multZ (pos (S y0)) (addZ y z)) (addZ (multZ (pos (S y0)) y) (multZ (pos (S y0)) z)) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
do 3 rewrite multZ_eq3.
(* Goal: @eq Z (posOZ (Init.Nat.mul (S n) (S O))) (multZ (pos n) IZ) *)
(* Goal: forall (n0 : nat) (_ : @eq Z (posOZ (Init.Nat.mul (S n) (S n0))) (multZ (pos n) (pos n0))), @eq Z (posOZ (Init.Nat.mul (S n) (S (S n0)))) (multZ (pos n) (pos (S n0))) *)
rewrite H1.
(* Goal: @eq Z (addZ (addZ (multZ (pos y0) y) (multZ (pos y0) z)) (addZ y z)) (addZ (addZ (multZ (pos y0) y) y) (addZ (multZ (pos y0) z) z)) *)
(* Goal: forall n : nat, and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z))) *)
apply (add_add Z addZ addZ_commutativity addZ_associativity).
(* neg n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* neg O *)
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split.
(* Goal: @eq Z (multZ (addZ (neg O) y) z) (addZ (multZ (neg O) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (neg O) (addZ y z)) (addZ (multZ (neg O) y) (multZ (neg O) z)) *)
(* Goal: forall (n : nat) (_ : and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z)))), and (@eq Z (multZ (addZ (neg (S n)) y) z) (addZ (multZ (neg (S n)) z) (multZ y z))) (@eq Z (multZ (neg (S n)) (addZ y z)) (addZ (multZ (neg (S n)) y) (multZ (neg (S n)) z))) *)
rewrite addZ_eq4; rewrite multZ_eq4; rewrite (mult_predZ_l y z). 
(* Goal: @eq Z (addZ (multZ y z) (oppZ z)) (addZ (oppZ z) (multZ y z)) *)
(* Goal: @eq Z (multZ (neg O) (addZ y z)) (addZ (multZ (neg O) y) (multZ (neg O) z)) *)
(* Goal: forall (n : nat) (_ : and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z)))), and (@eq Z (multZ (addZ (neg (S n)) y) z) (addZ (multZ (neg (S n)) z) (multZ y z))) (@eq Z (multZ (neg (S n)) (addZ y z)) (addZ (multZ (neg (S n)) y) (multZ (neg (S n)) z))) *)
exact (addZ_commutativity (multZ y z) (oppZ z)).
(* Goal: @eq Z (multZ (neg O) (addZ y z)) (addZ (multZ (neg O) y) (multZ (neg O) z)) *)
(* Goal: forall (n : nat) (_ : and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z)))), and (@eq Z (multZ (addZ (neg (S n)) y) z) (addZ (multZ (neg (S n)) z) (multZ y z))) (@eq Z (multZ (neg (S n)) (addZ y z)) (addZ (multZ (neg (S n)) y) (multZ (neg (S n)) z))) *)
rewrite multZ_eq4.
(* Goal: @eq Z (oppZ (addZ y z)) (addZ (multZ (neg O) y) (multZ (neg O) z)) *)
(* Goal: forall (n : nat) (_ : and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z)))), and (@eq Z (multZ (addZ (neg (S n)) y) z) (addZ (multZ (neg (S n)) z) (multZ y z))) (@eq Z (multZ (neg (S n)) (addZ y z)) (addZ (multZ (neg (S n)) y) (multZ (neg (S n)) z))) *)
apply (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity y z I I).
(* neg (S y0) *)
(* Goal: forall (n : nat) (_ : and (@eq Z (multZ (addZ (neg n) y) z) (addZ (multZ (neg n) z) (multZ y z))) (@eq Z (multZ (neg n) (addZ y z)) (addZ (multZ (neg n) y) (multZ (neg n) z)))), and (@eq Z (multZ (addZ (neg (S n)) y) z) (addZ (multZ (neg (S n)) z) (multZ y z))) (@eq Z (multZ (neg (S n)) (addZ y z)) (addZ (multZ (neg (S n)) y) (multZ (neg (S n)) z))) *)
intros y0 H.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split.
(* -> *)
(* Goal: @eq Z (multZ (addZ (neg (S y0)) y) z) (addZ (multZ (neg (S y0)) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (neg (S y0)) (addZ y z)) (addZ (multZ (neg (S y0)) y) (multZ (neg (S y0)) z)) *)
rewrite (tech_add_neg_predZ y0 y); rewrite (mult_predZ_l (addZ (neg y0) y) z).
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
elim H; intros. rewrite H0.
(* Goal: @eq Z (addZ (addZ (multZ (neg y0) z) (multZ y z)) (oppZ z)) (addZ (multZ (neg (S y0)) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (neg (S y0)) (addZ y z)) (addZ (multZ (neg (S y0)) y) (multZ (neg (S y0)) z)) *)
elim (addZ_associativity (multZ (neg y0) z) (multZ y z) (oppZ z)).
(* Goal: @eq Z (addZ (multZ (neg y0) z) (addZ (multZ y z) (oppZ z))) (addZ (multZ (neg (S y0)) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (neg (S y0)) (addZ y z)) (addZ (multZ (neg (S y0)) y) (multZ (neg (S y0)) z)) *)
elim (addZ_commutativity (oppZ z) (multZ y z)).
(* Goal: @eq Z (addZ (multZ (neg y0) z) (addZ (oppZ z) (multZ y z))) (addZ (multZ (neg (S y0)) z) (multZ y z)) *)
(* Goal: @eq Z (multZ (neg (S y0)) (addZ y z)) (addZ (multZ (neg (S y0)) y) (multZ (neg (S y0)) z)) *)
rewrite (addZ_associativity (multZ (neg y0) z) (oppZ z) (multZ y z)).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (tech_mult_negZ y0 z); reflexivity.
(* <- *)
(* Goal: @eq Z (multZ (neg (S y0)) (addZ y z)) (addZ (multZ (neg (S y0)) y) (multZ (neg (S y0)) z)) *)
rewrite (tech_mult_negZ y0 (addZ y z)); rewrite (tech_mult_negZ y0 y).
(* Goal: @eq Z (posOZ (Init.Nat.mul (S n) (S O))) (multZ (pos n) IZ) *)
(* Goal: forall (n0 : nat) (_ : @eq Z (posOZ (Init.Nat.mul (S n) (S n0))) (multZ (pos n) (pos n0))), @eq Z (posOZ (Init.Nat.mul (S n) (S (S n0)))) (multZ (pos n) (pos (S n0))) *)
rewrite (tech_mult_negZ y0 z); elim H; intros; rewrite H1.
elim
 (add_add Z addZ addZ_commutativity addZ_associativity 
    (multZ (neg y0) y) (multZ (neg y0) z) (oppZ y) 
    (oppZ z)).
(* Goal: @eq Z (addZ (addZ (multZ (neg y0) y) (multZ (neg y0) z)) (oppZ (addZ y z))) (addZ (addZ (multZ (neg y0) y) (multZ (neg y0) z)) (addZ (oppZ y) (oppZ z))) *)
elim (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity y z I I).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
Qed.

(****************)
Lemma mult_oppZ_r : forall x y : Z, multZ x (oppZ y) = oppZ (multZ x y).

(* Goal: forall x y : Z, @eq Z (multZ x (oppZ y)) (oppZ (multZ x y)) *)
intros; case x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) (multZ y z)) (multZ (multZ (pos n) y) z)), @eq Z (multZ (pos (S n)) (multZ y z)) (multZ (multZ (pos (S n)) y) z) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (multZ y z)) (multZ (multZ (neg n) y) z) *)
intros y0 H; do 2 rewrite (tech_mult_posZ y0).
rewrite
 (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity 
    (multZ (pos y0) y) y I I).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim H; reflexivity.
(* neg n *)
(* Goal: forall n m : nat, @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m))) *)
intros; elim n.
(* neg O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* neg (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (multZ y z)) (multZ (multZ (neg n) y) z)), @eq Z (multZ (neg (S n)) (multZ y z)) (multZ (multZ (neg (S n)) y) z) *)
intros y0 H; do 2 rewrite (tech_mult_negZ y0).
rewrite
 (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity 
    (multZ (neg y0) y) (oppZ y) I I).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim H; reflexivity.
Qed.

(****************)
Lemma mult_oppZ_l : forall x y : Z, multZ (oppZ x) y = oppZ (multZ x y).

(* Goal: forall x y : Z, @eq Z (multZ (oppZ x) y) (oppZ (multZ x y)) *)
simple destruct y.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
rewrite (mult_OZ (oppZ x)); rewrite (mult_OZ x); reflexivity.
(* pos n *)
(* Goal: forall n : nat, @eq Z (multZ (oppZ x) (pos n)) (oppZ (multZ x (pos n))) *)
(* Goal: forall n : nat, @eq Z (multZ (oppZ x) (neg n)) (oppZ (multZ x (neg n))) *)
intros; elim (multZ_commutativity (pos n) (oppZ x)). 
(* Goal: @eq Z (multZ (pos n) (oppZ x)) (oppZ (multZ x (pos n))) *)
(* Goal: forall n : nat, @eq Z (multZ (oppZ x) (neg n)) (oppZ (multZ x (neg n))) *)
elim (multZ_commutativity (pos n) x); elim n.
(* pos O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) (multZ y z)) (multZ (multZ (pos n) y) z)), @eq Z (multZ (pos (S n)) (multZ y z)) (multZ (multZ (pos (S n)) y) z) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (multZ y z)) (multZ (multZ (neg n) y) z) *)
intros y0 H; do 2 rewrite (tech_mult_posZ y0).
rewrite H; symmetry  in |- *. 
exact
 (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity 
    (multZ (pos y0) x) x I I).
(* neg n *)
(* Goal: forall n : nat, @eq Z (multZ (oppZ x) (neg n)) (oppZ (multZ x (neg n))) *)
intros; elim (multZ_commutativity (neg n) (oppZ x)). 
(* Goal: @eq Z (multZ (neg n) (oppZ x)) (oppZ (multZ x (neg n))) *)
elim (multZ_commutativity (neg n) x); elim n.
(* neg O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* neg (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (multZ y z)) (multZ (multZ (neg n) y) z)), @eq Z (multZ (neg (S n)) (multZ y z)) (multZ (multZ (neg (S n)) y) z) *)
intros y0 H; do 2 rewrite (tech_mult_negZ y0).
rewrite H; symmetry  in |- *.
exact
 (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity 
    (multZ (neg y0) x) (oppZ x) I I).
Qed.

(********************)
Lemma tech_multZ_negO : forall x : Z, multZ (neg 0) x = oppZ x.

Proof multZ_eq4.

(***********************)
Lemma tech_mult_pos_posZ :
 forall n m : nat, multZ (pos n) (pos m) = pos (n * m + (n + m)).

(* Goal: forall n m : nat, @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m))) *)
intros; elim n.
(* O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* S y *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) (pos m)) (pos (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m)))), @eq Z (multZ (pos (S n)) (pos m)) (pos (Init.Nat.add (Init.Nat.mul (S n) m) (Init.Nat.add (S n) m))) *)
intros y H; rewrite (tech_mult_posZ y (pos m)); rewrite H.
(* Goal: @eq Z (addZ (pos (Init.Nat.add (Init.Nat.mul y m) (Init.Nat.add y m))) (pos m)) (pos (Init.Nat.add (Init.Nat.mul (S y) m) (Init.Nat.add (S y) m))) *)
rewrite (tech_add_pos_posZ (y * m + (y + m)) m).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (technical_lemma y m); reflexivity.
Qed.

(***********************)
Lemma tech_mult_neg_negZ :
 forall n m : nat, multZ (neg n) (neg m) = pos (n * m + (n + m)).

(* Goal: forall n m : nat, @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m))) *)
intros; elim n.
(* O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* S y *)
intros y H; rewrite (tech_mult_negZ y (neg m)); rewrite H;
 unfold oppZ in |- *.
(* Goal: @eq Z (addZ (pos (Init.Nat.add (Init.Nat.mul y m) (Init.Nat.add y m))) (pos m)) (pos (Init.Nat.add (Init.Nat.mul (S y) m) (Init.Nat.add (S y) m))) *)
rewrite (tech_add_pos_posZ (y * m + (y + m)) m).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (technical_lemma y m); reflexivity.
Qed.

(***********************)
Lemma tech_mult_pos_negZ :
 forall n m : nat, multZ (pos n) (neg m) = neg (n * m + (n + m)).

(* Goal: forall n m : nat, @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m))) *)
intros; elim n.
(* O *)
(* Goal: @eq Z (multZ (neg O) (pos m)) (neg (Init.Nat.add (Init.Nat.mul O m) (Init.Nat.add O m))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m)))), @eq Z (multZ (neg (S n)) (pos m)) (neg (Init.Nat.add (Init.Nat.mul (S n) m) (Init.Nat.add (S n) m))) *)
simpl in |- *; reflexivity.
(* S y *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) (neg m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m)))), @eq Z (multZ (pos (S n)) (neg m)) (neg (Init.Nat.add (Init.Nat.mul (S n) m) (Init.Nat.add (S n) m))) *)
intros y H; rewrite (tech_mult_posZ y (neg m)); rewrite H.
(* Goal: @eq Z (addZ (neg (Init.Nat.add (Init.Nat.mul y m) (Init.Nat.add y m))) (neg m)) (neg (Init.Nat.add (Init.Nat.mul (S y) m) (Init.Nat.add (S y) m))) *)
rewrite (tech_add_neg_negZ (y * m + (y + m)) m).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (technical_lemma y m); reflexivity.
Qed.

(***********************)
Lemma tech_mult_neg_posZ :
 forall n m : nat, multZ (neg n) (pos m) = neg (n * m + (n + m)).

(* Goal: forall n m : nat, @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m))) *)
intros; elim n.
(* O *)
(* Goal: @eq Z (multZ (neg O) (pos m)) (neg (Init.Nat.add (Init.Nat.mul O m) (Init.Nat.add O m))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (pos m)) (neg (Init.Nat.add (Init.Nat.mul n m) (Init.Nat.add n m)))), @eq Z (multZ (neg (S n)) (pos m)) (neg (Init.Nat.add (Init.Nat.mul (S n) m) (Init.Nat.add (S n) m))) *)
simpl in |- *; reflexivity.
(* S y *)
intros y H; rewrite (tech_mult_negZ y (pos m)); unfold oppZ in |- *;
 rewrite H.
(* Goal: @eq Z (addZ (neg (Init.Nat.add (Init.Nat.mul y m) (Init.Nat.add y m))) (neg m)) (neg (Init.Nat.add (Init.Nat.mul (S y) m) (Init.Nat.add (S y) m))) *)
rewrite (tech_add_neg_negZ (y * m + (y + m)) m).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (technical_lemma y m); reflexivity.
Qed.

(**************************)
Theorem multZ_associativity : associativity Z multZ.

(* Goal: forall x y : Z, @eq Z (multZ x (predZ y)) (addZ (multZ x y) (oppZ x)) *)
unfold associativity in |- *; intros; elim x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
unfold multZ in |- *; reflexivity.
(* pos (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (pos n) (multZ y z)) (multZ (multZ (pos n) y) z)), @eq Z (multZ (pos (S n)) (multZ y z)) (multZ (multZ (pos (S n)) y) z) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (multZ y z)) (multZ (multZ (neg n) y) z) *)
intros y0 H; do 2 rewrite (tech_mult_posZ y0).
(* Goal: @eq Z (addZ (multZ (neg y0) (multZ y z)) (oppZ (multZ y z))) (multZ (addZ (multZ (neg y0) y) (oppZ y)) z) *)
rewrite H; elim (mult_oppZ_l y z).
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
elim (mult_add_distributivity (multZ (pos y0) y) y z); intros. elim H0.
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* neg n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* neg O *)
simpl in |- *; symmetry  in |- *; exact (mult_oppZ_l y z).
(* neg (S y0) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (multZ y z)) (multZ (multZ (neg n) y) z)), @eq Z (multZ (neg (S n)) (multZ y z)) (multZ (multZ (neg (S n)) y) z) *)
intros y0 H; do 2 rewrite (tech_mult_negZ y0).
(* Goal: @eq Z (addZ (multZ (neg y0) (multZ y z)) (oppZ (multZ y z))) (multZ (addZ (multZ (neg y0) y) (oppZ y)) z) *)
rewrite H; elim (mult_oppZ_l y z).
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
elim (mult_add_distributivity (multZ (neg y0) y) (oppZ y) z); intros. elim H0.
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
Qed.

(*************)
Theorem Z_ring : is_ring Z IdZ addZ multZ OZ oppZ.

(* Goal: is_ring Z IdZ addZ multZ OZ oppZ *)
unfold is_ring in |- *.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split. exact addZ_commutativity.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split. exact Z_group.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split. unfold intern in |- *. intros. exact I.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split. exact multZ_associativity. exact mult_add_distributivity.
Qed.

(*********************************)
Theorem Z_unitary_commutative_ring :
 is_unitary_commutative_ring Z IdZ addZ multZ OZ IZ oppZ.

(* Goal: is_unitary_commutative_ring Z IdZ addZ multZ OZ IZ oppZ *)
unfold is_unitary_commutative_ring in |- *.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split. exact Z_ring.
(* Goal: and (commutativity Z multZ) (neutral Z IdZ multZ IZ) *)
split. exact multZ_commutativity. exact multZ_neutral.
Qed.

(* Z is an integral domain *)
(********************)
Lemma tech_integ_posZ :
 forall (n : nat) (x : Z), multZ (pos n) x = OZ -> x = OZ.

(* Goal: forall (n : nat) (x : Z) (_ : @eq Z (multZ (neg n) x) OZ), @eq Z x OZ *)
intros n x; elim x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n0 *)
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros n0; rewrite (tech_mult_pos_posZ n n0); intros.
(* Goal: @eq Z (neg n0) OZ *)
absurd (pos (n * n0 + (n + n0)) = OZ). discriminate. exact H.
(* neg n0 *)
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros n0; rewrite (tech_mult_pos_negZ n n0); intros.
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
absurd (neg (n * n0 + (n + n0)) = OZ). discriminate. exact H.
Qed.

(********************)
Lemma tech_integ_negZ :
 forall (n : nat) (x : Z), multZ (neg n) x = OZ -> x = OZ.

(* Goal: forall (n : nat) (x : Z) (_ : @eq Z (multZ (neg n) x) OZ), @eq Z x OZ *)
intros n x; elim x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n0 *)
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros n0; rewrite (tech_mult_neg_posZ n n0); intros.
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
absurd (neg (n * n0 + (n + n0)) = OZ). discriminate. exact H.
(* neg n0 *)
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros n0; rewrite (tech_mult_neg_negZ n n0); intros.
(* Goal: @eq Z (neg n0) OZ *)
absurd (pos (n * n0 + (n + n0)) = OZ). discriminate. exact H.
Qed.

(*****************)
Theorem integrityZ : integrity Z multZ OZ.

(* Goal: integrity Z multZ OZ *)
unfold integrity in |- *; intros a b; elim a.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
intros; left; reflexivity.
(* pos n *)
(* Goal: @eq nat (S n0) O *)
(* Goal: forall (n1 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.mul n1 (S n)), @eq Z (neg n0) (multZ (pos n) (negOZ n1))) (_ : @eq nat (S n0) (Init.Nat.mul (S n1) (S n))), @eq Z (neg n0) (multZ (pos n) (negOZ (S n1))) *)
intros; right; apply (tech_integ_posZ n b); exact H.
(* neg n *)
(* Goal: @eq nat (S n0) O *)
(* Goal: forall (n1 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.mul n1 (S n)), @eq Z (neg n0) (multZ (pos n) (negOZ n1))) (_ : @eq nat (S n0) (Init.Nat.mul (S n1) (S n))), @eq Z (neg n0) (multZ (pos n) (negOZ (S n1))) *)
intros; right; apply (tech_integ_negZ n b); exact H.
Qed.

(************************)
Lemma tech_mult_pos_succZ :
 forall n m : nat, posOZ (S n * S m) = multZ (pos n) (pos m).

(* Goal: forall n m : nat, @eq Z (posOZ (Init.Nat.mul (S n) (S m))) (multZ (pos n) (pos m)) *)
intros; elim m.
(* O *)
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
elim multZ_neutral; intros; elim (H0 (pos n) I); intros. 
(* Goal: forall (n1 : nat) (n : Z), @eq Z (multZ (neg (S n1)) n) (addZ (multZ (neg n1) n) (oppZ n)) *)
replace (pos 0) with IZ; auto.
(* Goal: @eq Z (posOZ (Init.Nat.mul (S n) (S O))) (multZ (pos n) IZ) *)
(* Goal: forall (n0 : nat) (_ : @eq Z (posOZ (Init.Nat.mul (S n) (S n0))) (multZ (pos n) (pos n0))), @eq Z (posOZ (Init.Nat.mul (S n) (S (S n0)))) (multZ (pos n) (pos (S n0))) *)
rewrite H1.
(* Goal: @eq Z (posOZ (Init.Nat.mul (S n) (S O))) (pos n) *)
(* Goal: forall (n0 : nat) (_ : @eq Z (posOZ (Init.Nat.mul (S n) (S n0))) (multZ (pos n) (pos n0))), @eq Z (posOZ (Init.Nat.mul (S n) (S (S n0)))) (multZ (pos n) (pos (S n0))) *)
elim (mult_commut 1 (S n)). rewrite (mult_neutr (S n)). 
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
unfold posOZ in |- *; reflexivity.
(* S y *)
(* Goal: forall (n0 : nat) (_ : @eq Z (posOZ (Init.Nat.mul (S n) (S n0))) (multZ (pos n) (pos n0))), @eq Z (posOZ (Init.Nat.mul (S n) (S (S n0)))) (multZ (pos n) (pos (S n0))) *)
intros y H; elim (multZ_commutativity (pos (S y)) (pos n)).
rewrite (tech_mult_posZ y (pos n));
 elim (multZ_commutativity (pos n) (pos y)).
(* Goal: @eq Z (posOZ (Init.Nat.mul (S n) (S (S y)))) (addZ (multZ (pos n) (pos y)) (pos n)) *)
elim H; elim (mult_n_Sm (S n) (S y)); elim (plus_n_Sm (S n * S y) n).
(* Goal: @eq Z (posOZ (S (Init.Nat.add (Init.Nat.mul (S n) (S y)) n))) (addZ (posOZ (Init.Nat.mul (S n) (S y))) (pos n)) *)
elim (mult_n_Sm (S n) y); elim (plus_n_Sm (S n * y) n).
(* Goal: @eq Z (posOZ (S (Init.Nat.add (S (Init.Nat.add (Init.Nat.mul (S n) y) n)) n))) (addZ (posOZ (S (Init.Nat.add (Init.Nat.mul (S n) y) n))) (pos n)) *)
unfold posOZ in |- *; rewrite (tech_add_pos_posZ (S n * y + n) n).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
Qed.

(************************)
Lemma tech_mult_pos_succZ2 :
 forall n m : nat, multZ (pos n) (pos m) = pos (S n * m + n).

(* Goal: forall n m : nat, @eq Z (multZ (pos n) (pos m)) (pos (Init.Nat.add (Init.Nat.mul (S n) m) n)) *)
intros; elim (tech_mult_pos_succZ n m).
simpl in |- *; elim (mult_n_Sm n m); elim (plus_assoc m (n * m) n);
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
 reflexivity. 
Qed.

(**************)
Lemma tech_div1 :
 forall n0 n q r : nat,
 S n0 = q * S n + r -> pos n0 = addZ (multZ (pos n) (posOZ q)) (posOZ r).

(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ q)) (posOZ r)) *)
intros n0 n q r; elim q.
(* O O *)
(* Goal: forall (n1 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n1 (S n)) r), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n1)) (posOZ r))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n1) (S n)) r)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n1))) (posOZ r)) *)
elim r.
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
intros; absurd (S n0 = 0). discriminate. exact H.
(* O (S y) *)
(* Goal: forall (n1 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul O (S n)) n1), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ O)) (posOZ n1))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul O (S n)) (S n1))), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ O)) (posOZ (S n1))) *)
(* Goal: forall (n1 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n1 (S n)) r), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n1)) (posOZ r))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n1) (S n)) r)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n1))) (posOZ r)) *)
intros y H; unfold posOZ in |- *; rewrite (mult_OZ (pos n)).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
simpl in |- *; intros; elim (eq_add_S n0 y H0); reflexivity.
(* (S n) O *)
(* Goal: forall (n1 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n1 (S n)) r), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n1)) (posOZ r))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n1) (S n)) r)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n1))) (posOZ r)) *)
elim r.
(* Goal: forall (n1 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n1 (S n)) O), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n1)) (posOZ O))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n1) (S n)) O)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n1))) (posOZ O)) *)
(* Goal: forall (n1 : nat) (_ : forall (n2 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n2 (S n)) n1), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n2)) (posOZ n1))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n2) (S n)) n1)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n2))) (posOZ n1))) (n2 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n2 (S n)) (S n1)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n2)) (posOZ (S n1)))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n2) (S n)) (S n1))), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n2))) (posOZ (S n1))) *)
intros y H; unfold posOZ in |- *; elim (plus_n_O (S y * S n)).
(* Goal: forall _ : @eq nat (S n0) (Init.Nat.mul (S y) (S n)), @eq Z (pos n0) (addZ (multZ (pos n) (pos y)) OZ) *)
(* Goal: forall (n1 : nat) (_ : forall (n2 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n2 (S n)) n1), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n2)) (posOZ n1))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n2) (S n)) n1)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n2))) (posOZ n1))) (n2 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n2 (S n)) (S n1)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n2)) (posOZ (S n1)))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n2) (S n)) (S n1))), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n2))) (posOZ (S n1))) *)
rewrite (add_OZ (multZ (pos n) (pos y))); elim (tech_mult_pos_succZ n y).
elim (mult_commut (S n) (S y)); intros; elim H0; unfold posOZ in |- *;
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
 reflexivity.
(* (S n) (S y) *)
(* Goal: forall (n1 : nat) (_ : forall (n2 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n2 (S n)) n1), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n2)) (posOZ n1))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n2) (S n)) n1)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n2))) (posOZ n1))) (n2 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n2 (S n)) (S n1)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n2)) (posOZ (S n1)))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n2) (S n)) (S n1))), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n2))) (posOZ (S n1))) *)
intros y H y0 H0; unfold posOZ in |- *; elim (plus_n_Sm (S y0 * S n) y).
(* Goal: forall _ : @eq nat (S n0) (S (Init.Nat.add (Init.Nat.mul (S y0) (S n)) y)), @eq Z (pos n0) (addZ (multZ (pos n) (pos y0)) (pos y)) *)
intros; rewrite (eq_add_S n0 (S y0 * S n + y) H1).
(* Goal: @eq Z (pos (Init.Nat.add (Init.Nat.mul (S y0) (S n)) y)) (addZ (multZ (pos n) (pos y0)) (pos y)) *)
rewrite (tech_mult_pos_succZ2 n y0).
(* Goal: @eq Z (pos (Init.Nat.add (Init.Nat.mul (S y0) (S n)) y)) (addZ (pos (Init.Nat.add (Init.Nat.mul (S n) y0) n)) (pos y)) *)
rewrite (tech_add_pos_posZ (S n * y0 + n) y).
(* Goal: @eq Z (multZ (neg O) (predZ y)) (addZ (multZ (neg O) y) (oppZ (neg O))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n)))), @eq Z (multZ (neg (S n)) (predZ y)) (addZ (multZ (neg (S n)) y) (oppZ (neg (S n)))) *)
elim (plus_comm n (S n * y0)); elim (mult_commut y0 (S n)); simpl in |- *.
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
Qed.

(**************)
Lemma tech_div2 :
 forall n0 n q : nat, S n0 = q * S n -> neg n0 = multZ (pos n) (negOZ q).

(* Goal: forall (n0 n q : nat) (_ : @eq nat (S n0) (Init.Nat.mul q (S n))), @eq Z (neg n0) (multZ (pos n) (negOZ q)) *)
intros n0 n q; elim q.
(* O *)
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
simpl in |- *; intros; absurd (S n0 = 0). discriminate. exact H.
(* S y *)
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros y H; unfold negOZ in |- *. rewrite (tech_mult_pos_negZ n y); intros.
(* Goal: @eq Z (neg n0) (neg (Init.Nat.add (Init.Nat.mul n y) (Init.Nat.add n y))) *)
simpl in H0; rewrite (eq_add_S _ _ H0).
(* Goal: @eq Z (neg (Init.Nat.add n (Init.Nat.mul y (S n)))) (neg (Init.Nat.add (Init.Nat.mul n y) (Init.Nat.add n y))) *)
elim (mult_commut (S n) y); simpl in |- *; elim (plus_comm (n + y) (n * y)).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (plus_assoc n y (n * y)); reflexivity.
Qed.

(***************)
Lemma tech_div31 :
 forall n q : nat,
 addZ (oppZ (multZ (pos n) (pos q))) (pos n) = oppZ (multZ (pos n) (posOZ q)).

(* Goal: forall n q : nat, @eq Z (addZ (oppZ (multZ (pos n) (pos q))) (pos n)) (oppZ (multZ (pos n) (posOZ q))) *)
intros; elim q.
(* O *)
(* Goal: @eq Z (addZ (oppZ (multZ (pos n) (pos O))) (pos n)) (oppZ (multZ (pos n) (posOZ O))) *)
(* Goal: forall (n0 : nat) (_ : @eq Z (addZ (oppZ (multZ (pos n) (pos n0))) (pos n)) (oppZ (multZ (pos n) (posOZ n0)))), @eq Z (addZ (oppZ (multZ (pos n) (pos (S n0)))) (pos n)) (oppZ (multZ (pos n) (posOZ (S n0)))) *)
unfold posOZ in |- *; rewrite (mult_OZ (pos n)). 
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
cut (IZ = pos 0); intros. elim H. rewrite (mult_IZ (pos n)).
(* Goal: @eq Z (multZ (neg n0) y) (addZ (multZ (neg n0) y) (addZ (oppZ y) y)) *)
elim (addZ_opposite (pos n) I); intros; elim H1; intros; elim H3; intros.
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
rewrite H5; reflexivity. reflexivity.
(* S y *)
intros y H; unfold posOZ in |- *;
 elim (multZ_commutativity (pos (S y)) (pos n)).
(* Goal: @eq Z (addZ (oppZ (multZ (pos (S y)) (pos n))) (pos n)) (oppZ (multZ (pos n) (pos y))) *)
rewrite (tech_mult_posZ y (pos n)).
rewrite
 (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity
    (multZ (pos y) (pos n)) (pos n) I I).
elim
 (addZ_associativity (oppZ (multZ (pos y) (pos n))) (oppZ (pos n)) (pos n)).
(* Goal: @eq Z (multZ (neg n0) y) (addZ (multZ (neg n0) y) (addZ (oppZ y) y)) *)
elim (addZ_opposite (pos n) I); intros; elim H1; intros; elim H3; intros.
(* Goal: @eq Z (addZ (oppZ (multZ (pos y) (pos n))) (addZ (oppZ (pos n)) (pos n))) (oppZ (multZ (pos n) (pos y))) *)
rewrite H5; rewrite (add_OZ (oppZ (multZ (pos y) (pos n)))).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (multZ_commutativity (pos y) (pos n)); reflexivity.
Qed.

(***************)
Lemma tech_div32 :
 forall n q r : nat, S n > r -> pos (n - r) = addZ (pos n) (oppZ (posOZ r)).

(* Goal: forall (n1 : nat) (_ : forall _ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul n1 (S n)) r), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ n1)) (posOZ r))) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul (S n1) (S n)) r)), @eq Z (pos n0) (addZ (multZ (pos n) (posOZ (S n1))) (posOZ r)) *)
intros n q r; elim r.
(* O *)
unfold posOZ in |- *; unfold oppZ in |- *; rewrite (add_OZ (pos n));
 elim (minus_n_O n).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* S y *)
intros y H; unfold posOZ in |- *; unfold oppZ in |- *; symmetry  in |- *. 
(* Goal: @eq Z (addZ (pos n) (neg y)) (pos (Init.Nat.sub n (S y))) *)
exact (tech_add_pos_neg_posZ n y (gt_S_n y n H0)).
Qed.

(**************)
Lemma tech_div3 :
 forall n0 n q r : nat,
 S n0 = q * S n + r ->
 S n > r -> neg n0 = addZ (multZ (pos n) (neg q)) (pos (n - r)).

(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros.
(* Goal: @eq Z (neg n0) (addZ (multZ (pos n) (neg q)) (pos (Init.Nat.sub n r))) *)
elim (tech_opp_pos_negZ q); intros; elim H1.
(* Goal: @eq Z (neg n0) (addZ (multZ (pos n) (oppZ (pos q))) (pos (Init.Nat.sub n r))) *)
rewrite (mult_oppZ_r (pos n) (pos q)); rewrite (tech_div32 n q r H0).
rewrite
 (addZ_associativity (oppZ (multZ (pos n) (pos q))) (pos n) (oppZ (posOZ r)))
 .
(* Goal: @eq Z (neg n0) (addZ (addZ (oppZ (multZ (pos n) (pos q))) (pos n)) (oppZ (posOZ r))) *)
rewrite (tech_div31 n q).
elim
 (opp_add Z IdZ addZ OZ oppZ Z_group addZ_commutativity
    (multZ (pos n) (posOZ q)) (posOZ r) I I).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim (tech_div1 n0 n q r H); reflexivity.
Qed.

(**************)
Lemma tech_div4 :
 forall n0 n q r : nat,
 S n0 = q * S n + r -> pos n0 = addZ (multZ (neg n) (negOZ q)) (posOZ r).

(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros; cut (multZ (neg n) (negOZ q) = multZ (pos n) (posOZ q)); intros.
(* Goal: @eq Z (pos n0) (addZ (multZ (neg n) (negOZ q)) (posOZ r)) *)
(* Goal: @eq Z (multZ (neg n) (negOZ q)) (multZ (pos n) (posOZ q)) *)
rewrite H0; intros; exact (tech_div1 n0 n q r H).
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
cut (negOZ q = oppZ (posOZ q)); intros. rewrite H0.
(* Goal: @eq Z (neg n0) (multZ (neg n) (oppZ (negOZ q))) *)
(* Goal: @eq Z (posOZ q) (oppZ (negOZ q)) *)
elim (tech_opp_pos_negZ n); intros; elim H1.
(* Goal: @eq Z (multZ (oppZ (pos n)) (oppZ (posOZ q))) (multZ (pos n) (posOZ q)) *)
(* Goal: @eq Z (negOZ q) (oppZ (posOZ q)) *)
apply (mult_opp_opp Z IdZ addZ multZ OZ oppZ Z_ring (pos n) (posOZ q) I I).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim q; reflexivity.
Qed.

(**************)
Lemma tech_div5 :
 forall n0 n q : nat, S n0 = q * S n -> neg n0 = multZ (neg n) (posOZ q).

(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros; cut (posOZ q = oppZ (negOZ q)); intros. rewrite H0.
(* Goal: @eq Z (neg n0) (multZ (neg n) (oppZ (negOZ q))) *)
(* Goal: @eq Z (posOZ q) (oppZ (negOZ q)) *)
elim (tech_opp_pos_negZ n); intros; elim H1.
(* Goal: @eq Z (neg n0) (multZ (oppZ (pos n)) (oppZ (negOZ q))) *)
(* Goal: @eq Z (posOZ q) (oppZ (negOZ q)) *)
rewrite (mult_opp_opp Z IdZ addZ multZ OZ oppZ Z_ring (pos n) (negOZ q) I I).
(* Goal: @eq Z (neg n0) (multZ (pos n) (negOZ q)) *)
(* Goal: @eq Z (posOZ q) (oppZ (negOZ q)) *)
exact (tech_div2 n0 n q H).
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
elim q; reflexivity.
Qed.

(**************)
Lemma tech_div6 :
 forall n0 n q r : nat,
 S n0 = q * S n + r ->
 S n > r -> neg n0 = addZ (multZ (neg n) (pos q)) (pos (n - r)).

(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros.
(* Goal: @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
elim (tech_opp_pos_negZ q); intros; elim H2.
(* Goal: @eq Z (neg n0) (addZ (multZ (neg n) (oppZ (neg q))) (pos (Init.Nat.sub n r))) *)
elim (tech_opp_pos_negZ n); intros; elim H3.
(* Goal: @eq Z (neg n0) (addZ (multZ (oppZ (pos n)) (oppZ (neg q))) (pos (Init.Nat.sub n r))) *)
rewrite (mult_opp_opp Z IdZ addZ multZ OZ oppZ Z_ring (pos n) (neg q) I I).
(* Goal: @eq Z (neg n0) (addZ (multZ (pos n) (neg q)) (pos (Init.Nat.sub n r))) *)
apply (tech_div3 n0 n q r H H0).
Qed.

(****************)
Lemma inversibleZ :
 forall x : Z, inversible Z multZ IZ x -> x = IZ \/ x = oppZ IZ.

(* Goal: forall x : Z, @eq Z (multZ x (sgnZ x)) (absZ x) *)
simple destruct x.
(* OZ *)
(* Goal: forall _ : inversible Z multZ IZ OZ, or (@eq Z OZ IZ) (@eq Z OZ (oppZ IZ)) *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (pos n)), or (@eq Z (pos n) IZ) (@eq Z (pos n) (oppZ IZ)) *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
intros; elim H; intros; elim H0; intros; elim H1.
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
left; reflexivity.
(* pos n *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* pos O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
intros; left; reflexivity.
(* pos (S y) *)
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros y H H0; elim H0; intros; elim H1; intros.
(* Goal: or (@eq Z (pos (S y)) IZ) (@eq Z (pos (S y)) (oppZ IZ)) *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
absurd (multZ (pos (S y)) x0 = IZ). elim x0.
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
rewrite (mult_OZ (pos (S y))). discriminate.
(* Goal: forall n : nat, not (@eq Z (multZ (pos (S y)) (pos n)) IZ) *)
(* Goal: forall n : nat, not (@eq Z (multZ (pos (S y)) (neg n)) IZ) *)
(* Goal: @eq Z (multZ (pos (S y)) x0) IZ *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
intros; rewrite (tech_mult_pos_posZ (S y) n0).
(* Goal: not (@eq Z (pos (Init.Nat.add (Init.Nat.mul (S y) n0) (Init.Nat.add (S y) n0))) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
elim (plus_comm (S y + n0) (S y * n0)).
(* Goal: @eq Z (multZ (neg O) (predZ y)) (addZ (multZ (neg O) y) (oppZ (neg O))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n)))), @eq Z (multZ (neg (S n)) (predZ y)) (addZ (multZ (neg (S n)) y) (oppZ (neg (S n)))) *)
elim (plus_assoc (S y) n0 (S y * n0)); simpl in |- *.
(* Goal: not (@eq Z (pos (S (Nat.add y (Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0)))))) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
apply (tech_pos_not_posZ (S (y + (n0 + (n0 + y * n0)))) 0).
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
discriminate.
(* Goal: forall n : nat, not (@eq Z (multZ (pos (S y)) (neg n)) IZ) *)
(* Goal: @eq Z (multZ (pos (S y)) x0) IZ *)
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
intros; rewrite (tech_mult_pos_negZ (S y) n0).
(* Goal: not (@eq Z (pos (Init.Nat.add (Init.Nat.mul (S y) n0) (Init.Nat.add (S y) n0))) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
elim (plus_comm (S y + n0) (S y * n0)).
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
elim (plus_assoc (S y) n0 (S y * n0)); simpl in |- *; discriminate.
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
exact H2.
(* neg n *) 
(* Goal: forall (n : nat) (_ : inversible Z multZ IZ (neg n)), or (@eq Z (neg n) IZ) (@eq Z (neg n) (oppZ IZ)) *)
simple induction n.
(* neg O *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
right; reflexivity.
(* neg (S y) *)
(* Goal: forall (n0 n q r : nat) (_ : @eq nat (S n0) (Init.Nat.add (Init.Nat.mul q (S n)) r)) (_ : gt (S n) r), @eq Z (neg n0) (addZ (multZ (neg n) (pos q)) (pos (Init.Nat.sub n r))) *)
intros y H H0; elim H0; intros; elim H1; intros.
(* Goal: not (@eq Z (multZ (neg (S y)) x0) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
absurd (multZ (neg (S y)) x0 = IZ). elim x0.
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
rewrite (mult_OZ (neg (S y))). discriminate.
(* Goal: forall n : nat, not (@eq Z (multZ (neg (S y)) (pos n)) IZ) *)
(* Goal: forall n : nat, not (@eq Z (multZ (neg (S y)) (neg n)) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
intros; rewrite (tech_mult_neg_posZ (S y) n0).
(* Goal: not (@eq Z (pos (Init.Nat.add (Init.Nat.mul (S y) n0) (Init.Nat.add (S y) n0))) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
elim (plus_comm (S y + n0) (S y * n0)).
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
elim (plus_assoc (S y) n0 (S y * n0)); simpl in |- *; discriminate.
(* Goal: forall n : nat, not (@eq Z (multZ (neg (S y)) (neg n)) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
intros; rewrite (tech_mult_neg_negZ (S y) n0).
(* Goal: not (@eq Z (pos (Init.Nat.add (Init.Nat.mul (S y) n0) (Init.Nat.add (S y) n0))) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
elim (plus_comm (S y + n0) (S y * n0)).
(* Goal: @eq Z (multZ (neg O) (predZ y)) (addZ (multZ (neg O) y) (oppZ (neg O))) *)
(* Goal: forall (n : nat) (_ : @eq Z (multZ (neg n) (predZ y)) (addZ (multZ (neg n) y) (oppZ (neg n)))), @eq Z (multZ (neg (S n)) (predZ y)) (addZ (multZ (neg (S n)) y) (oppZ (neg (S n)))) *)
elim (plus_assoc (S y) n0 (S y * n0)); simpl in |- *.
(* Goal: not (@eq Z (pos (S (Nat.add y (Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0)))))) IZ) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
apply (tech_pos_not_posZ (S (y + (n0 + (n0 + y * n0)))) 0).
(* Goal: not (@eq nat (S (Init.Nat.add y (Init.Nat.add n0 (Init.Nat.add n0 (Init.Nat.mul y n0))))) O) *)
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
discriminate.
(* Goal: @eq Z (multZ (neg (S y)) x0) IZ *)
exact H2.
Qed.

(************)
Lemma sgn_abs : forall x : Z, multZ x (sgnZ x) = absZ x.

(* Goal: forall x : Z, @eq Z (multZ x (sgnZ x)) (absZ x) *)
simple destruct x.
(* OZ *)
(* Goal: @eq Z (multZ OZ (sgnZ OZ)) (absZ OZ) *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
reflexivity.
(* pos n *)
(* Goal: forall n : nat, @eq Z (multZ (pos n) (sgnZ (pos n))) (absZ (pos n)) *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
intros; exact (mult_IZ (pos n)).
(* neg n *)
(* Goal: forall n : nat, @eq Z (multZ (neg n) (sgnZ (neg n))) (absZ (neg n)) *)
intros; exact (mult_mIZ (neg n)).
Qed.