(* 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                               *)
(*                                                                          *)
(****************************************************************************)
(*                                  Zgcd.v                                  *)
(****************************************************************************)
Require Export misc.
Require Export Zadd.
Require Export Zle.
Require Export Euclid.
Require Export Peano_dec.
Require Export Zrec.
Require Export Zmult.
Require Export Zdiv.

Unset Standard Proposition Elimination Names.

(***************************)
Lemma gcd_unicity_apart_sign :
 forall a b d1 d2 : Z,
 is_gcd Z IdZ multZ OZ a b d1 ->
 is_gcd Z IdZ multZ OZ a b d2 -> d2 = d1 \/ d2 = oppZ d1.

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros.
elim
 (gcd_unicity_apart_unities Z IdZ addZ multZ OZ IZ oppZ
    Z_unitary_commutative_ring integrityZ a b d1 d2 H H0).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (inversibleZ x); intros.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
left. elim H1; intros; elim H4; intros. rewrite H6. rewrite H2. 
(* Goal: @eq Z (multZ d1 IZ) d1 *)
(* Goal: or (@eq Z d2 d1) (@eq Z d2 (oppZ d1)) *)
(* Goal: inversible Z multZ IZ x *)
exact (mult_IZ d1).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
right. elim H1; intros; elim H4; intros. rewrite H6. rewrite H2.
(* Goal: @eq Z (multZ d1 (oppZ IZ)) (oppZ d1) *)
(* Goal: inversible Z multZ IZ x *)
simpl in |- *; exact (mult_mIZ d1).
(* Goal: inversible Z multZ IZ x *)
elim H1; intros; exact H2.
Qed.

(***********)
Lemma gcd_OZ_absZ : forall b : Z, is_gcd Z IdZ multZ OZ OZ b (absZ b).

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros. elim (abs_eq_or_oppZ b); intro y.
(* |b|=b *)
(* Goal: is_gcd Z IdZ multZ OZ OZ b (absZ b) *)
rewrite y.
(* Goal: is_gcd Z IdZ multZ OZ OZ b (oppZ b) *)
unfold is_gcd in |- *; split.
(* Goal: divide Z IdZ multZ OZ (oppZ b) OZ *)
(* Goal: and (divide Z IdZ multZ OZ (oppZ b) b) (forall (q : Z) (_ : divide Z IdZ multZ OZ q OZ) (_ : divide Z IdZ multZ OZ q b), divide Z IdZ multZ OZ q (oppZ b)) *)
unfold divide in |- *; unfold IdZ in |- *; split. exact I. split. exact I. left; reflexivity.
(* Goal: IdZ IZ *)
(* Goal: @eq Z x (multZ x IZ) *)
split; unfold divide in |- *; unfold IdZ in |- *. split. exact I. split. exact I.
(* Goal: or (@eq Z b OZ) (and (not (@eq Z (oppZ b) OZ)) (@ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))))) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
elim (eq_OZ_dec b); intro y0. 
(* Goal: or (@eq Z b OZ) (and (not (@eq Z (oppZ b) OZ)) (@ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))))) *)
(* Goal: or (@eq Z b OZ) (and (not (@eq Z (oppZ b) OZ)) (@ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))))) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
left; exact y0.
(* Goal: or (@eq Z b OZ) (and (not (@eq Z (oppZ b) OZ)) (@ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))))) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
right. split. exact y0. exists IZ. split. exact I. symmetry  in |- *; exact (mult_IZ b).
(* Goal: forall (q : Z) (_ : and True (and True (or (@eq Z OZ OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z OZ (multZ q q0)))))))) (_ : and True (and True (or (@eq Z b OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z b (multZ q q0)))))))), and True (and True (or (@eq Z b OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z b (multZ q q0))))))) *)
(* Goal: is_gcd Z IdZ multZ OZ OZ b (absZ b) *)
intros; exact H0.
(* |b|=(-b) *)
(* Goal: is_gcd Z IdZ multZ OZ OZ b (absZ b) *)
rewrite y.
(* Goal: is_gcd Z IdZ multZ OZ OZ b (oppZ b) *)
unfold is_gcd in |- *; split.
(* Goal: divide Z IdZ multZ OZ (oppZ b) OZ *)
(* Goal: and (divide Z IdZ multZ OZ (oppZ b) b) (forall (q : Z) (_ : divide Z IdZ multZ OZ q OZ) (_ : divide Z IdZ multZ OZ q b), divide Z IdZ multZ OZ q (oppZ b)) *)
unfold divide in |- *; unfold IdZ in |- *; split. exact I. split. exact I. left; reflexivity.
(* Goal: divide Z IdZ multZ OZ (oppZ b) OZ *)
(* Goal: and (divide Z IdZ multZ OZ (oppZ b) b) (forall (q : Z) (_ : divide Z IdZ multZ OZ q OZ) (_ : divide Z IdZ multZ OZ q b), divide Z IdZ multZ OZ q (oppZ b)) *)
split; unfold divide in |- *; unfold IdZ in |- *; split. exact I. split. exact I.
(* Goal: or (@eq Z b OZ) (and (not (@eq Z (oppZ b) OZ)) (@ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))))) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
elim (eq_OZ_dec b); intro y0. 
(* Goal: or (@eq Z b OZ) (and (not (@eq Z (oppZ b) OZ)) (@ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))))) *)
(* Goal: or (@eq Z b OZ) (and (not (@eq Z (oppZ b) OZ)) (@ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))))) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
left; exact y0.
(* Goal: or (@eq Z b OZ) (and (not (@eq Z (oppZ b) OZ)) (@ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))))) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
right. split.
(* Goal: not (@eq Z (oppZ b) OZ) *)
(* Goal: @ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
unfold not in |- *; intros; elim y0.
(* Goal: @eq Z b OZ *)
(* Goal: @ex Z (fun q : Z => and True (@eq Z b (multZ (oppZ b) q))) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
exact (opp_O Z IdZ addZ multZ OZ oppZ Z_ring b I H).
(* Goal: IdZ IZ *)
(* Goal: @eq Z x (multZ x IZ) *)
exists (oppZ IZ); split. exact I.
(* Goal: @eq Z b (multZ (oppZ b) (oppZ IZ)) *)
(* Goal: True *)
(* Goal: and True (or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0)))))) *)
rewrite (mult_opp_opp Z IdZ addZ multZ OZ oppZ Z_ring b IZ I I).
(* Goal: IdZ IZ *)
(* Goal: @eq Z x (multZ x IZ) *)
symmetry  in |- *; exact (mult_IZ b). exact I. split. exact I.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim H0; intros; elim H2; intros; elim H4; intros. rewrite H5. 
(* Goal: or (@eq Z (oppZ OZ) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ OZ) (multZ q q0))))) *)
(* Goal: or (@eq Z (oppZ b) OZ) (and (not (@eq Z q OZ)) (@ex Z (fun q0 : Z => and True (@eq Z (oppZ b) (multZ q q0))))) *)
left; reflexivity.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
right; split. elim H5; intros; exact H6. elim H5; intros; elim H7; intros.
(* Goal: IdZ IZ *)
(* Goal: @eq Z x (multZ x IZ) *)
exists (oppZ x). split. exact I. elim H8; intros; rewrite H10.
symmetry  in |- *; exact (mult_opp_r Z IdZ addZ multZ OZ oppZ Z_ring q x I I).
Qed.

(******************)
Inductive is_gcdZ : Z -> Z -> Z -> Prop :=
  | gcd_OZ : forall b : Z, is_gcdZ OZ b (absZ b)
  | gcd_mod :
      forall b a d q r : Z,
      b <> OZ -> is_diveuclZ a b q r -> is_gcdZ r b d -> is_gcdZ b a d.

(******************)
Definition have_gcdZ (a b : Z) := {d : Z | is_gcdZ a b d}.

Definition gcdZ_i (a b : Z) := exist (is_gcdZ a b).

(* Inductive have_gcdZ [a, b: Z]: Set
  := gcdZ_i: (d: Z) (is_gcdZ a b d) -> (have_gcdZ a b). *)

(*******************)
Definition P (a : Z) := forall b : Z, have_gcdZ a b.

Lemma acc_P : forall n : Z, (forall m : Z, lt_absZ m n -> P m) -> P n.
Proof.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
  intros. case (eq_OZ_dec n); intro. unfold P in |- *. intro.
(* Goal: have_gcdZ n b *)
(* Goal: P n *)
  split with (absZ b). rewrite e. apply (gcd_OZ b).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
  unfold P in |- *; intro. elim (divZ b n). intros. cut (lt_absZ r n); intros.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
  elim (H r H0 n). intros. split with x.
(* Goal: is_gcdZ n b x *)
(* Goal: lt_absZ r n *)
(* Goal: not (@eq Z n OZ) *)
  apply gcd_mod with (2 := i); trivial. inversion i. decompose [and] H1.
(* Goal: lt_absZ rem q *)
(* Goal: not (@eq Z q OZ) *)
  unfold lt_absZ in |- *. rewrite (tech_le_pos_abs r H2). exact H4. exact n0.
Qed.

Lemma gcdZ_exists : forall a b : Z, have_gcdZ a b.
Proof.
(* Goal: forall a b : Z, have_gcdZ a b *)
  exact (recZ P acc_P).
Qed.

(****************)
Lemma gcdZ_is_gcd :
 forall a b d : Z, is_gcdZ a b d -> is_gcd Z IdZ multZ OZ a b d.

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros. elim H; intros. apply (gcd_OZ_absZ b0). unfold is_gcd in |- *.
(* Goal: and (IdZ IZ) (@eq Z x (multZ x IZ)) *)
split. elim H3; intros; elim H5; intros; exact H6.
(* Goal: and (IdZ IZ) (@eq Z x (multZ x IZ)) *)
split. elim H1; intros; elim H5; intros; elim H7; intros; rewrite H9.
(* Goal: divide Z IdZ multZ OZ d0 (addZ (multZ b0 q) r) *)
(* Goal: forall (q : Z) (_ : divide Z IdZ multZ OZ q b0) (_ : divide Z IdZ multZ OZ q a0), divide Z IdZ multZ OZ q d0 *)
apply (div_add Z IdZ addZ multZ OZ oppZ Z_ring (multZ b0 q) r d0).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim H3; intros; elim H11; intros. 
(* Goal: divide Z IdZ multZ OZ d0 (multZ b0 q) *)
(* Goal: divide Z IdZ multZ OZ d0 r *)
(* Goal: forall (q : Z) (_ : divide Z IdZ multZ OZ q b0) (_ : divide Z IdZ multZ OZ q a0), divide Z IdZ multZ OZ q d0 *)
exact (div_mult Z IdZ addZ multZ OZ oppZ Z_ring b0 q d0 H12 I).
(* Goal: divide Z IdZ multZ OZ d0 r *)
(* Goal: forall (q : Z) (_ : divide Z IdZ multZ OZ q b0) (_ : divide Z IdZ multZ OZ q a0), divide Z IdZ multZ OZ q d0 *)
elim H3; intros; exact H10.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros. elim H3; intros; elim H7; intros. apply (H9 q0).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
cut (r = addZ a0 (oppZ (multZ b0 q))); intros. rewrite H10.
(* Goal: divide Z IdZ multZ OZ q0 (addZ a0 (oppZ (multZ b0 q))) *)
(* Goal: @eq Z r (addZ a0 (oppZ (multZ b0 q))) *)
(* Goal: divide Z IdZ multZ OZ q0 b0 *)
apply (div_add Z IdZ addZ multZ OZ oppZ Z_ring a0 (oppZ (multZ b0 q)) q0 H5).
(* Goal: divide Z IdZ multZ OZ q0 (oppZ (multZ b0 q)) *)
(* Goal: @eq Z r (addZ a0 (oppZ (multZ b0 q))) *)
(* Goal: divide Z IdZ multZ OZ q0 b0 *)
apply (div_opp Z IdZ addZ multZ OZ oppZ Z_ring (multZ b0 q) q0).
(* Goal: divide Z IdZ multZ OZ q0 (multZ b0 q) *)
(* Goal: @eq Z r (addZ a0 (oppZ (multZ b0 q))) *)
(* Goal: divide Z IdZ multZ OZ q0 b0 *)
exact (div_mult Z IdZ addZ multZ OZ oppZ Z_ring b0 q q0 H4 I).
(* Goal: @eq Z r (addZ a0 (oppZ (multZ b0 q))) *)
(* Goal: divide Z IdZ multZ OZ q0 b0 *)
elim H1; intros; elim H11; intros; elim H13; intros; rewrite H15.
(* Goal: @eq Z r (addZ (addZ (multZ b0 q) r) (oppZ (multZ b0 q))) *)
(* Goal: divide Z IdZ multZ OZ q0 b0 *)
elim (addZ_commutativity r (multZ b0 q)).
(* Goal: @eq Z r (addZ (addZ r (multZ b0 q)) (oppZ (multZ b0 q))) *)
(* Goal: divide Z IdZ multZ OZ q0 b0 *)
elim (addZ_associativity r (multZ b0 q) (oppZ (multZ b0 q))).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (addZ_opposite (multZ b0 q) I); intros. 
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim H17; intros. elim H19; intros. rewrite H20. symmetry  in |- *. exact (add_OZ r).
(* Goal: divide Z IdZ multZ OZ q0 b0 *)
exact H4.
Qed.

(*************)
Definition gcdZ (a b : Z) := pi1 Z (is_gcdZ a b) (gcdZ_exists a b).

(*******************)
Theorem gcdZ_correct : forall a b : Z, is_gcdZ a b (gcdZ a b).
Proof fun a b : Z => pi2 Z (is_gcdZ a b) (gcdZ_exists a b).

(*********************)
Lemma positive_is_gcdZ : forall a b d : Z, is_gcdZ a b d -> leZ OZ d.

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros; elim H; intros. apply (sign_absZ b0). exact H3.
Qed.

(********************)
Lemma unicity_is_gcdZ :
 forall a b d1 d2 : Z, is_gcdZ a b d1 -> is_gcdZ a b d2 -> d2 = d1.

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros.
elim
 (gcd_unicity_apart_sign a b d1 d2 (gcdZ_is_gcd a b d1 H)
    (gcdZ_is_gcd a b d2 H0)).
(* Goal: forall _ : @eq Z d2 d1, @eq Z d2 d1 *)
(* Goal: forall _ : @eq Z d2 (oppZ d1), @eq Z d2 d1 *)
intros; exact H1.
intros;
 apply
  (le_opp_OZ2 d2 d1 H1 (positive_is_gcdZ a b d2 H0)
     (positive_is_gcdZ a b d1 H)).
Qed.

(*****************)
Lemma gcdZ_is_gcdZ : forall a b d : Z, is_gcdZ a b d -> d = gcdZ a b.

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros. apply (unicity_is_gcdZ a b (gcdZ a b) d (gcdZ_correct a b) H).
Qed.

(*************)
Lemma gcd_modZ :
 forall a b q r : Z, b <> OZ -> is_diveuclZ a b q r -> gcdZ r b = gcdZ b a. 

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros. apply (gcdZ_is_gcdZ b a (gcdZ r b)).
(* Goal: is_gcdZ b a (gcdZ r b) *)
apply (gcd_mod b a (gcdZ r b) q r H H0 (gcdZ_correct r b)).
Qed.

(*********************************)
Inductive verify_BezoutZ (a b : Z) : Set :=
    Bezout_i :
      forall u v : Z,
      addZ (multZ a u) (multZ b v) = gcdZ a b -> verify_BezoutZ a b.

(********************)
Definition Q (a : Z) := forall b : Z, verify_BezoutZ a b.

Lemma acc_Q : forall n : Z, (forall m : Z, lt_absZ m n -> Q m) -> Q n.
Proof.
(* Goal: forall b : Z, have_gcdZ n b *)
(* Goal: P n *)
  intros q f. case (eq_OZ_dec q); intro. unfold Q in |- *; intro b.
(* Goal: @eq Z (addZ (addZ (multZ rem u) (multZ q v)) (addZ (oppZ (multZ q (multZ div u))) (multZ (multZ q div) u))) (gcdZ q b) *)
(* Goal: lt_absZ rem q *)
(* Goal: not (@eq Z q OZ) *)
  split with IZ (sgnZ b). rewrite e. simpl in |- *. rewrite (sgn_abs b).
(* Goal: Q q *)
  apply (gcdZ_is_gcdZ OZ b (absZ b)); apply gcd_OZ. unfold Q in |- *; intro b.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
  elim (divZ b q). intros div rem; intros. cut (lt_absZ rem q); intros.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
  elim (f rem H q). intros. split with (addZ v (oppZ (multZ div u))) u.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
  elim i. intros. elim H1. intros. elim H3. intros. pattern b at 1 in |- *.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
  rewrite H5. elim (mult_add_distributivity q v (oppZ (multZ div u))); intros.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
  rewrite H7. elim (mult_add_distributivity (multZ q div) rem u); intros.
(* Goal: @eq Z (addZ (addZ (multZ q v) (multZ q (oppZ (multZ div u)))) (multZ (addZ (multZ q div) rem) u)) (gcdZ q b) *)
(* Goal: lt_absZ rem q *)
(* Goal: not (@eq Z q OZ) *)
  rewrite H8. rewrite (mult_opp_r Z IdZ addZ multZ OZ oppZ Z_ring q (multZ div u) I I).
(* Goal: @eq Z (addZ (addZ (multZ q v) (oppZ (multZ q (multZ div u)))) (addZ (multZ (multZ q div) u) (multZ rem u))) (gcdZ q b) *)
(* Goal: lt_absZ rem q *)
(* Goal: not (@eq Z q OZ) *)
  elim (addZ_commutativity (multZ rem u) (multZ (multZ q div) u)).
  rewrite
   (add_add Z addZ addZ_commutativity addZ_associativity 
      (multZ q v) (oppZ (multZ q (multZ div u))) (multZ rem u)
      (multZ (multZ q div) u)).
(* Goal: @eq Z (addZ (addZ (multZ rem u) (multZ q v)) (addZ (oppZ (multZ q (multZ div u))) (multZ (multZ q div) u))) (gcdZ q b) *)
(* Goal: lt_absZ rem q *)
(* Goal: not (@eq Z q OZ) *)
    elim (addZ_commutativity (multZ rem u) (multZ q v)). rewrite e.
(* Goal: @eq Z (addZ (gcdZ rem q) (addZ (oppZ (multZ q (multZ div u))) (multZ (multZ q div) u))) (gcdZ q b) *)
(* Goal: lt_absZ rem q *)
(* Goal: not (@eq Z q OZ) *)
    elim (multZ_associativity q div u).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
    elim (addZ_opposite (multZ q (multZ div u)) I); intros.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
    elim H11; intros; elim H13; intros. rewrite H15.
(* Goal: @eq Z (addZ (gcdZ rem q) OZ) (gcdZ q b) *)
(* Goal: lt_absZ rem q *)
(* Goal: not (@eq Z q OZ) *)
    rewrite (add_OZ (gcdZ rem q)).
(* Goal: lt_absZ rem q *)
(* Goal: not (@eq Z q OZ) *)
    exact (gcd_modZ b q div rem n i). unfold lt_absZ in |- *.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
    elim i; intros; elim H0; intros. rewrite (tech_le_pos_abs rem H1).
(* Goal: ltZ rem (absZ q) *)
(* Goal: not (@eq Z q OZ) *)
    elim H2; trivial. exact n.
Qed.

Lemma Bezout_exists : forall a b : Z, verify_BezoutZ a b.
Proof.
(* Goal: forall a b : Z, verify_BezoutZ a b *)
  exact (recZ Q acc_Q).
Qed.

(******************)
Definition congruentZ (x y n : Z) :=
  divide Z IdZ multZ OZ n (addZ x (oppZ y)).

(*****************)
Lemma divide_selfZ : forall x : Z, divide Z IdZ multZ OZ x x.

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros. unfold divide in |- *. split. exact I. split. exact I.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (eq_OZ_dec x); intros. left; exact a.
(* Goal: IdZ IZ *)
(* Goal: @eq Z x (multZ x IZ) *)
right; split. exact b. exists IZ. split. exact I. symmetry  in |- *; exact (mult_IZ x).
Qed.

(**********************************)
Theorem chinese_remaindering_theorem :
 forall a b x y : Z,
 gcdZ a b = IZ -> {z : Z | congruentZ z x a /\ congruentZ z y b}.

(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
intros. elim (Bezout_exists a b); intros.
(* Goal: @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
exists (addZ (multZ x (multZ b v)) (multZ y (multZ a u))).
(* Goal: and (IdZ IZ) (@eq Z x (multZ x IZ)) *)
unfold congruentZ in |- *; split.
(* congruentZ (z, x, a) *)
(* Goal: divide Z IdZ multZ OZ a (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ x)) *)
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
replace (multZ b v) with (addZ IZ (oppZ (multZ a u))).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (mult_add_distributivity x IZ (oppZ (multZ a u))); intros.
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (addZ IZ (oppZ (multZ b v))))) (oppZ y)) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
rewrite H1; clear H0 H1. rewrite (mult_IZ x).
(* Goal: divide Z IdZ multZ OZ a (addZ (addZ (addZ x (multZ x (oppZ (multZ a u)))) (multZ y (multZ a u))) (oppZ x)) *)
(* Goal: @eq Z (addZ IZ (oppZ (multZ a u))) (multZ b v) *)
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
elim (mult_opp_r Z IdZ addZ multZ OZ oppZ Z_ring a u I I).
(* Goal: divide Z IdZ multZ OZ a (addZ (addZ (addZ x (multZ x (multZ a (oppZ u)))) (multZ y (multZ a u))) (oppZ x)) *)
(* Goal: @eq Z (addZ IZ (oppZ (multZ a u))) (multZ b v) *)
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
rewrite (multZ_associativity x a (oppZ u)). elim (multZ_commutativity a x).
(* Goal: divide Z IdZ multZ OZ a (addZ (addZ (addZ x (multZ (multZ a x) (oppZ u))) (multZ y (multZ a u))) (oppZ x)) *)
(* Goal: @eq Z (addZ IZ (oppZ (multZ a u))) (multZ b v) *)
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
elim (multZ_associativity a x (oppZ u)). rewrite (multZ_associativity y a u).
(* Goal: divide Z IdZ multZ OZ a (addZ (addZ (addZ x (multZ a (multZ x (oppZ u)))) (multZ (multZ y a) u)) (oppZ x)) *)
(* Goal: @eq Z (addZ IZ (oppZ (multZ a u))) (multZ b v) *)
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
elim (multZ_commutativity a y). elim (multZ_associativity a y u).
elim
 (addZ_associativity x (multZ a (multZ x (oppZ u))) (multZ a (multZ y u))).
elim
 (addZ_commutativity
    (addZ (multZ a (multZ x (oppZ u))) (multZ a (multZ y u))) x).
elim
 (addZ_associativity
    (addZ (multZ a (multZ x (oppZ u))) (multZ a (multZ y u))) x 
    (oppZ x)).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (addZ_opposite x I); intros. elim H1; intros. elim H3; intros. 
(* Goal: @eq Z (multZ a u) (addZ (multZ a u) (addZ (multZ b v) (oppZ (multZ b v)))) *)
rewrite H4; clear H0 H1 H2 H3 H4 H5.
(* Goal: divide Z IdZ multZ OZ a (addZ (addZ (multZ a (multZ x (oppZ u))) (multZ a (multZ y u))) OZ) *)
(* Goal: @eq Z (addZ IZ (oppZ (multZ a u))) (multZ b v) *)
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
rewrite (add_OZ (addZ (multZ a (multZ x (oppZ u))) (multZ a (multZ y u)))).
apply
 (div_add Z IdZ addZ multZ OZ oppZ Z_ring (multZ a (multZ x (oppZ u)))
    (multZ a (multZ y u)) a).
apply
 (div_mult Z IdZ addZ multZ OZ oppZ Z_ring a (multZ x (oppZ u)) a
    (divide_selfZ a) I).
apply
 (div_mult Z IdZ addZ multZ OZ oppZ Z_ring a (multZ y u) a (divide_selfZ a) I).
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
elim H. elim e.
(* Goal: @eq Z (addZ (addZ (multZ a u) (multZ b v)) (oppZ (multZ a u))) (multZ b v) *)
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
elim (addZ_commutativity (multZ b v) (multZ a u)).
(* Goal: @eq Z (addZ (addZ (multZ b v) (multZ a u)) (oppZ (multZ a u))) (multZ b v) *)
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
elim (addZ_associativity (multZ b v) (multZ a u) (oppZ (multZ a u))).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (addZ_opposite (multZ a u) I); intros. elim H1; intros. elim H3; intros.
(* Goal: @eq Z (multZ a u) (addZ (multZ a u) (addZ (multZ b v) (oppZ (multZ b v)))) *)
rewrite H4; clear H0 H1 H2 H3 H4 H5. exact (add_OZ (multZ b v)).
(* congruentZ (z y b) *)
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
cut (multZ a u = addZ IZ (oppZ (multZ b v))); intros.
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (multZ a u))) (oppZ y)) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
rewrite H0; clear H0.
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (mult_add_distributivity y IZ (oppZ (multZ b v))); intros.
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (multZ y (addZ IZ (oppZ (multZ b v))))) (oppZ y)) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
rewrite H1; clear H0 H1. rewrite (mult_IZ y).
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (addZ y (multZ y (oppZ (multZ b v))))) (oppZ y)) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
elim (mult_opp_r Z IdZ addZ multZ OZ oppZ Z_ring b v I I).
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (addZ y (multZ y (multZ b (oppZ v))))) (oppZ y)) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
rewrite (multZ_associativity y b (oppZ v)). elim (multZ_commutativity b y).
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ x (multZ b v)) (addZ y (multZ (multZ b y) (oppZ v)))) (oppZ y)) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
elim (multZ_associativity b y (oppZ v)). rewrite (multZ_associativity x b v).
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ (multZ x b) v) (addZ y (multZ b (multZ y (oppZ v))))) (oppZ y)) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
elim (multZ_commutativity b x). elim (multZ_associativity b x v).
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ b (multZ x v)) (addZ y (multZ b (multZ y (oppZ v))))) (oppZ y)) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
elim (addZ_commutativity (multZ b (multZ y (oppZ v))) y).
rewrite
 (addZ_associativity (multZ b (multZ x v)) (multZ b (multZ y (oppZ v))) y)
 .
elim
 (addZ_associativity
    (addZ (multZ b (multZ x v)) (multZ b (multZ y (oppZ v)))) y 
    (oppZ y)).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (addZ_opposite y I); intros. elim H1; intros. elim H3; intros.
(* Goal: @eq Z (multZ a u) (addZ (multZ a u) (addZ (multZ b v) (oppZ (multZ b v)))) *)
rewrite H4; clear H0 H1 H2 H3 H4 H5.
(* Goal: divide Z IdZ multZ OZ b (addZ (addZ (multZ b (multZ x v)) (multZ b (multZ y (oppZ v)))) OZ) *)
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
rewrite (add_OZ (addZ (multZ b (multZ x v)) (multZ b (multZ y (oppZ v))))).
apply
 (div_add Z IdZ addZ multZ OZ oppZ Z_ring (multZ b (multZ x v))
    (multZ b (multZ y (oppZ v))) b).
apply
 (div_mult Z IdZ addZ multZ OZ oppZ Z_ring b (multZ x v) b (divide_selfZ b) I).
apply
 (div_mult Z IdZ addZ multZ OZ oppZ Z_ring b (multZ y (oppZ v)) b
    (divide_selfZ b) I).
(* Goal: @eq Z (multZ a u) (addZ IZ (oppZ (multZ b v))) *)
elim H. elim e.
(* Goal: @eq Z (multZ a u) (addZ (addZ (multZ a u) (multZ b v)) (oppZ (multZ b v))) *)
elim (addZ_associativity (multZ a u) (multZ b v) (oppZ (multZ b v))).
(* Goal: forall (a b x y : Z) (_ : @eq Z (gcdZ a b) IZ), @sig Z (fun z : Z => and (congruentZ z x a) (congruentZ z y b)) *)
elim (addZ_opposite (multZ b v) I); intros. elim H1; intros. elim H3; intros.
(* Goal: @eq Z (multZ a u) (addZ (multZ a u) (addZ (multZ b v) (oppZ (multZ b v)))) *)
rewrite H4; clear H0 H1 H2 H3 H4 H5. symmetry  in |- *; exact (add_OZ (multZ a u)).
Qed.
