(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   gcd.
   Greatest common divisor.
   
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
 *)

Require Import ZArith.
Require Import Wf_nat.

Require Import lemmas.
Require Import natZ.
Require Import divides.
Require Import modulo.

(** * Linear combinations. *)

Definition LinComb (c x y : Z) :=
  exists a : Z, (exists b : Z, c = (x * a + y * b)%Z).

Definition LinCombMod (c x y : Z) (n : nat) :=
  exists a : Z, (exists b : Z, Mod c (x * a + y * b) n).

Definition ZLinCombMod (c x y n : Z) :=
  exists a : Z, (exists b : Z, ZMod c (x * a + y * b) n).

Lemma lincombmodzlincombmod :
 forall (c x y : Z) (n : nat),
 LinCombMod c x y n -> ZLinCombMod c x y (Z_of_nat n).
Proof.
(* Goal: forall (c x y : Z) (n : nat) (_ : LinCombMod c x y n), ZLinCombMod c x y (Z.of_nat n) *)
   unfold LinCombMod, ZLinCombMod in |- *.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros. elim H. intros z Hz. exists z.
(* Goal: @ex Z (fun b : Z => ZMod c (Z.add (Z.mul x z) (Z.mul y b)) (Z.of_nat n)) *)
   elim Hz. intros b Hb. exists b.
(* Goal: ZMod c (Z.add (Z.mul x z) (Z.mul y b)) (Z.of_nat n) *)
   apply modzmod. assumption.
Qed.

Lemma zlincombmodlincombmod :
 forall c x y n : Z, ZLinCombMod c x y n -> LinCombMod c x y (Zabs_nat n).
Proof.
(* Goal: forall (c x y n : Z) (_ : ZLinCombMod c x y n), LinCombMod c x y (Z.abs_nat n) *)
   unfold ZLinCombMod, LinCombMod in |- *.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros. elim H. intros a Ha. exists a.
(* Goal: forall (x0 : Z) (_ : ZMod c (Z.add (Z.mul x a) (Z.mul y x0)) n), @ex Z (fun b : Z => Mod c (Z.add (Z.mul x a) (Z.mul y b)) (Z.abs_nat n)) *)
   elim Ha. intros b Hb. exists b.
(* Goal: gcd x y d *)
   apply zmodmod. assumption.
Qed.

(** * Greatest common divisor. *)

Definition common_div (x y : Z) (d : nat) :=
  Divides d (Zabs_nat x) /\ Divides d (Zabs_nat y).

Definition gcd (x y : Z) (d : nat) :=
  common_div x y d /\ (forall e : nat, common_div x y e -> e <= d).

Lemma gcd_unq :
 forall (d1 d2 : nat) (x y : Z), gcd x y d1 -> gcd x y d2 -> d1 = d2.
Proof.
(* Goal: forall (d : nat) (x y q r : Z) (_ : gcd x y d) (_ : @eq Z x (Z.add (Z.mul q y) r)), gcd r y d *)
   unfold gcd in |- *.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: LinComb (Z.of_nat d) x y *)
(* Goal: Z.le Z0 x *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   elim H.
(* Goal: Divides e d *)
   elim H0.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: @eq nat d1 d2 *)
   apply le_antisym.
(* Goal: le e d *)
   apply H2.
(* Goal: gcd x y d *)
   assumption.
(* Goal: le d2 d1 *)
   apply H4.
(* Goal: gcd x y d *)
   assumption.
Qed.

Lemma gcd_sym : forall (d : nat) (x y : Z), gcd x y d -> gcd y x d.
Proof.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   unfold gcd in |- *. unfold common_div in |- *. intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H. intros. elim H0. intros.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split. split.
(* Goal: gcd x y d *)
   assumption. assumption.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H4. intros. apply H1. split.
(* Goal: gcd x y d *)
   assumption. assumption.
Qed.

Lemma gcd_opp_l : forall (d : nat) (x y : Z), gcd x y d -> gcd (- x) y d.
Proof.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   unfold gcd in |- *. unfold common_div in |- *. intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H. intros. elim H0. intros.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split.
(* Goal: Divides d (Z.abs_nat (Z.opp y)) *)
(* Goal: forall (e : nat) (_ : and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat (Z.opp y)))), le e d *)
   rewrite <- abs_opp.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   assumption.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H4. intros.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   apply H1. split.
(* Goal: Divides e (Z.abs_nat y) *)
   rewrite abs_opp.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   assumption.
Qed.

Lemma gcd_opp_r : forall (d : nat) (x y : Z), gcd x y d -> gcd x (- y) d.
Proof.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   unfold gcd in |- *. unfold common_div in |- *. intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H. intros. elim H0. intros.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split.
(* Goal: gcd x y d *)
   assumption.
(* Goal: Divides d (Z.abs_nat (Z.opp y)) *)
(* Goal: forall (e : nat) (_ : and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat (Z.opp y)))), le e d *)
   rewrite <- abs_opp.
(* Goal: gcd x y d *)
   assumption.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H4. intros.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   apply H1. split.
(* Goal: gcd x y d *)
   assumption.
(* Goal: Divides e (Z.abs_nat y) *)
   rewrite abs_opp.
(* Goal: gcd x y d *)
   assumption.
Qed.

Lemma gcd_0_l : forall d : nat, d > 0 -> gcd 0 (Z_of_nat d) d.
Proof.
(* Goal: forall (d : nat) (x y q r : Z) (_ : gcd x y d) (_ : @eq Z x (Z.add (Z.mul q y) r)), gcd r y d *)
   unfold gcd in |- *. unfold common_div in |- *.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split. split.
(* Goal: Divides d (Z.abs_nat Z0) *)
(* Goal: Divides d (Z.abs_nat (Z.of_nat d)) *)
(* Goal: forall (e : nat) (_ : and (Divides e (Z.abs_nat Z0)) (Divides e (Z.abs_nat (Z.of_nat d)))), le e d *)
   split with 0. simpl in |- *. rewrite <- mult_n_O. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt x Z0 *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   split with 1. simpl in |- *. rewrite <- mult_n_Sm.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt x Z0 *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   rewrite <- mult_n_O. simpl in |- *. rewrite abs_inj. reflexivity.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: le e d *)
   apply div_le.
(* Goal: gcd x y d *)
   assumption.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H0. intros.
(* Goal: gcd x y d *)
   rewrite abs_inj in H2. assumption.
Qed.

Lemma gcd_0_r : forall d : nat, d > 0 -> gcd (Z_of_nat d) 0 d.
Proof.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros. apply gcd_sym. apply gcd_0_l. assumption.
Qed.

(** * Euclid's theorem. *)

Lemma euclid_gcd1 :
 forall (d : nat) (x y q r : Z), gcd x y d -> x = (q * y + r)%Z -> gcd r y d.
Proof.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   unfold gcd in |- *. unfold common_div in |- *. intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H. intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H1. intros.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split.
(* Goal: Divides d (Z.abs_nat r) *)
(* Goal: Divides d (Z.abs_nat y) *)
(* Goal: forall (e : nat) (_ : and (Divides e (Z.abs_nat r)) (Divides e (Z.abs_nat y))), le e d *)
   rewrite <- (abs_inj d). apply zdivdiv.
(* Goal: ZDivides (Z.of_nat d) r *)
(* Goal: Divides d (Z.abs_nat y) *)
(* Goal: forall (e : nat) (_ : and (Divides e (Z.abs_nat r)) (Divides e (Z.abs_nat y))), le e d *)
   apply zdiv_plus_r with (q * y)%Z.
(* Goal: @eq Z (Z.of_nat d) (Z.mul (Z.of_nat X) (Zpos xH)) *)
(* Goal: forall (n : nat) (_ : and (le O (S n)) (and (lt (S n) X) (@eq nat y (Init.Nat.add (Init.Nat.mul q X) (S n))))), @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   rewrite Zmult_comm. apply zdiv_mult_compat_l.
(* Goal: gcd x y d *)
   apply divzdiv. rewrite abs_inj. assumption.
(* Goal: gcd x y d *)
   rewrite <- H0. apply divzdiv. rewrite abs_inj. assumption.
(* Goal: gcd x y d *)
   assumption.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H5. intros.
(* Goal: le e d *)
   apply H2.
(* Goal: and (Divides e (Z.abs_nat x)) (Divides e (Z.abs_nat y)) *)
   split.
(* Goal: Divides (Z.abs_nat (Z.of_nat e)) (Z.abs_nat x) *)
(* Goal: Divides e (Z.abs_nat y) *)
   rewrite <- (abs_inj e). apply zdivdiv.
(* Goal: ZDivides (Z.of_nat e) x *)
(* Goal: Divides e (Z.abs_nat y) *)
   rewrite H0.
(* Goal: ZDivides (Z.of_nat e) (Z.add (Z.mul q y) r) *)
(* Goal: Divides e (Z.abs_nat y) *)
   apply zdiv_plus_compat.
(* Goal: @eq Z (Z.of_nat d) (Z.mul (Z.of_nat X) (Zpos xH)) *)
(* Goal: forall (n : nat) (_ : and (le O (S n)) (and (lt (S n) X) (@eq nat y (Init.Nat.add (Init.Nat.mul q X) (S n))))), @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   rewrite Zmult_comm. apply zdiv_mult_compat_l.
(* Goal: Divides (Z.abs_nat (Z.of_nat e)) (Z.abs_nat r) *)
(* Goal: Divides e (Z.abs_nat y) *)
   apply divzdiv. rewrite abs_inj.
(* Goal: gcd x y d *)
   assumption.
(* Goal: Divides (Z.abs_nat (Z.of_nat e)) (Z.abs_nat r) *)
(* Goal: Divides e (Z.abs_nat y) *)
   apply divzdiv. rewrite abs_inj.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   assumption.
Qed.

Theorem euclid_gcd :
 forall (d1 d2 : nat) (x y q r : Z),
 x = (q * y + r)%Z -> gcd x y d1 -> gcd r y d2 -> d1 = d2.
Proof.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: @eq nat d1 d2 *)
   apply (gcd_unq d1 d2 r y).
(* Goal: gcd r y d1 *)
(* Goal: gcd r y d2 *)
   apply euclid_gcd1 with x q.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   assumption.
Qed.

(** * Greatest common divisor can be written as linear combination. *)

Lemma gcd_lincomb_nat :
 forall x y d : nat,
 x > 0 ->
 gcd (Z_of_nat x) (Z_of_nat y) d ->
 LinComb (Z_of_nat d) (Z_of_nat x) (Z_of_nat y).
Proof.
(* Goal: forall (x y d : nat) (_ : gt x O) (_ : gcd (Z.of_nat x) (Z.of_nat y) d), LinComb (Z.of_nat d) (Z.of_nat x) (Z.of_nat y) *)
   unfold LinComb in |- *. intro x.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   apply (lt_wf_ind x). intros X IH. intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim (div_rem X y). intro q. intros. elim H1.
(* Goal: forall (x : nat) (_ : and (le O x) (and (lt x X) (@eq nat y (Init.Nat.add (Init.Nat.mul q X) x)))), @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   intro r. case r.

   (* case r = 0 *)
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H2. intros. elim H4. intros.
(* Goal: @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: forall (n : nat) (_ : and (le O (S n)) (and (lt (S n) X) (@eq nat y (Init.Nat.add (Init.Nat.mul q X) (S n))))), @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   rewrite <- plus_n_O in H6.
(* Goal: @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: forall (n : nat) (_ : and (le O (S n)) (and (lt (S n) X) (@eq nat y (Init.Nat.add (Init.Nat.mul q X) (S n))))), @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   split with 1%Z. split with 0%Z.
(* Goal: @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) (Zpos xH)) (Z.mul (Z.of_nat y) Z0)) *)
(* Goal: forall (n : nat) (_ : and (le O (S n)) (and (lt (S n) X) (@eq nat y (Init.Nat.add (Init.Nat.mul q X) (S n))))), @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   rewrite <- Zmult_0_r_reverse. rewrite <- Zplus_0_r_reverse.
(* Goal: @eq Z (Z.of_nat d) (Z.mul (Z.of_nat X) (Zpos xH)) *)
(* Goal: forall (n : nat) (_ : and (le O (S n)) (and (lt (S n) X) (@eq nat y (Init.Nat.add (Init.Nat.mul q X) (S n))))), @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   rewrite Zmult_comm. rewrite Zmult_1_l.
(* Goal: @eq Z (Z.of_nat y) (Z.of_nat (Init.Nat.add (Init.Nat.mul q X) (S r1))) *)
(* Goal: gt X O *)
   apply Znat.inj_eq.
(* Goal: @eq nat d X *)
(* Goal: forall (n : nat) (_ : and (le O (S n)) (and (lt (S n) X) (@eq nat y (Init.Nat.add (Init.Nat.mul q X) (S n))))), @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   apply (euclid_gcd d X (Z_of_nat y) (Z_of_nat X) (Z_of_nat q) 0).
(* Goal: gcd x y d *)
   rewrite <- Zplus_0_r_reverse. rewrite <- Znat.inj_mult. apply Znat.inj_eq. assumption.
(* Goal: gcd x y d *)
   apply gcd_sym. assumption. apply gcd_0_l. assumption.

   (* case r > 0 *)
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intro r1. intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H2. intros. elim H4. intros.
(* Goal: @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt X O *)
   elim (IH (S r1) H5 X d).
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intro delta. intros. elim H7. intro gamma. intros.
(* Goal: @ex Z (fun a : Z => @ex Z (fun b : Z => @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) a) (Z.mul (Z.of_nat y) b)))) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   split with (gamma - Z_of_nat q * delta)%Z. split with delta.
(* Goal: @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat X) (Z.sub gamma (Z.mul (Z.of_nat q) delta))) (Z.mul (Z.of_nat y) delta)) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   rewrite H6. rewrite H8.
(* Goal: @eq Z (Z.add (Z.mul (Z.of_nat (S r1)) delta) (Z.mul (Z.of_nat X) gamma)) (Z.add (Z.mul (Z.of_nat X) (Z.sub gamma (Z.mul (Z.of_nat q) delta))) (Z.mul (Z.of_nat (Init.Nat.add (Init.Nat.mul q X) (S r1))) delta)) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   unfold Zminus in |- *. rewrite Zmult_plus_distr_r.
(* Goal: @eq Z (Z.add (Z.mul (Z.of_nat (S r1)) delta) (Z.mul (Z.of_nat X) gamma)) (Z.add (Z.add (Z.mul (Z.of_nat X) gamma) (Z.mul (Z.of_nat X) (Z.opp (Z.mul (Z.of_nat q) delta)))) (Z.mul (Z.of_nat (Init.Nat.add (Init.Nat.mul q X) (S r1))) delta)) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   rewrite Znat.inj_plus. rewrite Zmult_plus_distr_l.
(* Goal: @eq Z (Z.add (Z.mul (Z.of_nat (S r1)) delta) (Z.mul (Z.of_nat X) gamma)) (Z.add (Z.add (Z.mul (Z.of_nat X) gamma) (Z.mul (Z.of_nat X) (Z.opp (Z.mul (Z.of_nat q) delta)))) (Z.add (Z.mul (Z.of_nat (Init.Nat.mul q X)) delta) (Z.mul (Z.of_nat (S r1)) delta))) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   rewrite Znat.inj_mult. rewrite <- Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.add (Z.mul (Z.of_nat (S r1)) delta) (Z.mul (Z.of_nat X) gamma)) (Z.add (Z.add (Z.mul (Z.of_nat X) gamma) (Z.mul (Z.of_nat X) (Z.mul (Z.opp (Z.of_nat q)) delta))) (Z.add (Z.mul (Z.mul (Z.of_nat q) (Z.of_nat X)) delta) (Z.mul (Z.of_nat (S r1)) delta))) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   rewrite (Zmult_assoc (Z_of_nat X)).
(* Goal: @eq Z (Z.add (Z.mul (Z.of_nat (S r1)) delta) (Z.mul (Z.of_nat X) gamma)) (Z.add (Z.add (Z.mul (Z.of_nat X) gamma) (Z.mul (Z.mul (Z.of_nat X) (Z.opp (Z.of_nat q))) delta)) (Z.add (Z.mul (Z.mul (Z.of_nat q) (Z.of_nat X)) delta) (Z.mul (Z.of_nat (S r1)) delta))) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   rewrite (Zmult_comm (Z_of_nat X) (- Z_of_nat q)).
(* Goal: @eq Z (Z.add (Z.opp (Z.mul x alpha)) (Z.mul y beta)) (Z.add (Z.mul (Z.opp alpha) x) (Z.mul y beta)) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   rewrite Zopp_mult_distr_l_reverse. rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.add (Z.mul (Z.of_nat (S r1)) delta) (Z.mul (Z.of_nat X) gamma)) (Z.add (Z.add (Z.mul (Z.of_nat X) gamma) (Z.opp (Z.mul (Z.mul (Z.of_nat q) (Z.of_nat X)) delta))) (Z.add (Z.mul (Z.mul (Z.of_nat q) (Z.of_nat X)) delta) (Z.mul (Z.of_nat (S r1)) delta))) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   rewrite (Zplus_assoc_reverse (Z_of_nat X * gamma)).
(* Goal: @eq Z (Z.of_nat y) (Z.add (Z.mul (Z.of_nat q) (Z.of_nat X)) (Z.of_nat (S r1))) *)
(* Goal: gt X O *)
   rewrite <- Znat.inj_mult.
(* Goal: @eq Z (Z.add (Z.mul (Z.of_nat (S r1)) delta) (Z.mul (Z.of_nat X) gamma)) (Z.add (Z.mul (Z.of_nat X) gamma) (Z.add (Z.opp (Z.mul (Z.of_nat (Init.Nat.mul q X)) delta)) (Z.add (Z.mul (Z.of_nat (Init.Nat.mul q X)) delta) (Z.mul (Z.of_nat (S r1)) delta)))) *)
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   rewrite (Zplus_assoc (- (Z_of_nat (q * X) * delta))). 
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt x Z0 *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   rewrite Zplus_opp_l. simpl in |- *. apply Zplus_comm.
(* Goal: gt (S r1) O *)
(* Goal: gcd (Z.of_nat (S r1)) (Z.of_nat X) d *)
(* Goal: gt X O *)
   apply gt_Sn_O.
   apply
    (euclid_gcd1 d (Z_of_nat y) (Z_of_nat X) (Z_of_nat q) (Z_of_nat (S r1))).
(* Goal: gcd x y d *)
   apply gcd_sym. assumption.
(* Goal: gcd x y d *)
   rewrite <- Znat.inj_mult. rewrite <- Znat.inj_plus. apply Znat.inj_eq. assumption.
(* Goal: gcd x y d *)
   assumption.
Qed.

Lemma gcd_lincomb_pos :
 forall (x y : Z) (d : nat),
 (x > 0)%Z -> gcd x y d -> LinComb (Z_of_nat d) x y.
Proof.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: LinComb (Z.of_nat d) x y *)
   elim (Zle_or_lt 0 y).

   (* case 0 <= y *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   intro. rewrite <- (inj_abs_pos x). rewrite <- (inj_abs_pos y).
(* Goal: LinComb (Z.of_nat d) (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) *)
(* Goal: Z.ge y Z0 *)
(* Goal: Z.ge x Z0 *)
(* Goal: forall _ : Z.lt y Z0, LinComb (Z.of_nat d) x y *)
   apply gcd_lincomb_nat.
(* Goal: gt (Z.abs_nat x) O *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   change (Zabs_nat x > Zabs_nat 0) in |- *.
(* Goal: gcd x y d *)
   apply gtzgt. apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt x Z0 *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   rewrite inj_abs_pos. rewrite inj_abs_pos. assumption.
(* Goal: gcd x y d *)
   apply Zle_ge. assumption.
(* Goal: gcd x y d *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: gcd x y d *)
   apply Zle_ge. assumption.
(* Goal: gcd x y d *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.

   (* case y < 0 *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   intro. rewrite <- (inj_abs_pos x).
(* Goal: LinComb (Z.of_nat d) (Z.of_nat (Z.abs_nat x)) y *)
(* Goal: Z.ge x Z0 *)
   replace y with (- - y)%Z. rewrite <- (inj_abs_neg y).
(* Goal: LinComb (Z.of_nat d) (Z.of_nat (Z.abs_nat x)) (Z.opp (Z.of_nat (Z.abs_nat y))) *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   elim (gcd_lincomb_nat (Zabs_nat x) (Zabs_nat y) d).
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intro alpha. intros. elim H2. intro beta. intros.
(* Goal: LinComb (Z.of_nat d) (Z.of_nat (Z.abs_nat x)) (Z.opp (Z.of_nat (Z.abs_nat y))) *)
(* Goal: gt (Z.abs_nat x) O *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   split with alpha. split with (- beta)%Z.
(* Goal: @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat (Z.abs_nat x)) alpha) (Z.opp (Z.mul beta (Z.opp (Z.of_nat (Z.abs_nat y)))))) *)
(* Goal: gt (Z.abs_nat x) O *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   rewrite <- Zopp_mult_distr_r. rewrite (Zmult_comm (- Z_of_nat (Zabs_nat y))).
(* Goal: @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.of_nat (Z.abs_nat x)) alpha) (Z.opp (Z.mul beta (Z.opp (Z.of_nat (Z.abs_nat y)))))) *)
(* Goal: gt (Z.abs_nat x) O *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   rewrite <- Zopp_mult_distr_r. rewrite Zopp_involutive. rewrite (Zmult_comm beta).
(* Goal: gcd x y d *)
   assumption.
(* Goal: gt (Z.abs_nat x) O *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   change (Zabs_nat x > Zabs_nat 0) in |- *. apply gtzgt.
(* Goal: gcd x y d *)
   apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 Z0) Gt) *)
(* Goal: Z.gt x Z0 *)
(* Goal: gcd (Z.of_nat (Z.abs_nat x)) (Z.of_nat (Z.abs_nat y)) d *)
(* Goal: Z.lt y Z0 *)
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   rewrite inj_abs_pos. rewrite inj_abs_neg. apply gcd_opp_r. assumption.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: gcd x y d *)
   assumption.
(* Goal: @eq Z (Z.opp (Z.opp y)) y *)
(* Goal: Z.ge x Z0 *)
   apply Zopp_involutive.
(* Goal: gcd x y d *)
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.
Qed.

Theorem gcd_lincomb :
 forall (x y : Z) (d : nat),
 x <> 0%Z -> gcd x y d -> LinComb (Z_of_nat d) x y.
Proof.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   intros.
(* Goal: LinComb (Z.of_nat d) x y *)
   elim (Zle_or_lt 0 x).
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   intro.
(* Goal: LinComb (Z.of_nat d) x y *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   elim (Zle_lt_or_eq 0 x).

   (* case 0 < x *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   intro.
(* Goal: LinComb (Z.of_nat d) x y *)
(* Goal: forall _ : @eq Z Z0 x, LinComb (Z.of_nat d) x y *)
(* Goal: Z.le Z0 x *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   apply gcd_lincomb_pos.
(* Goal: Z.gt x Z0 *)
(* Goal: gcd x y d *)
(* Goal: forall _ : @eq Z Z0 x, LinComb (Z.of_nat d) x y *)
(* Goal: Z.le Z0 x *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   apply Zlt_gt.
(* Goal: gcd x y d *)
   assumption.
(* Goal: gcd x y d *)
   assumption.

   (* case 0 = x *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   intro.
(* Goal: LinComb (Z.of_nat d) x y *)
(* Goal: Z.le Z0 x *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   elim H.
(* Goal: @eq Z x Z0 *)
(* Goal: Z.le Z0 x *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   rewrite H2.
(* Goal: @eq Z (Z.add (Z.opp (Z.mul x alpha)) (Z.mul y beta)) (Z.add (Z.opp (Z.mul x alpha)) (Z.mul y beta)) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   reflexivity.
(* Goal: gcd x y d *)
   assumption.

   (* case 0 > x *)
(* Goal: forall _ : Z.lt x Z0, LinComb (Z.of_nat d) x y *)
   intro.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim (gcd_lincomb_pos (- x) y d). intro alpha. intros.
(* Goal: forall _ : @eq Z (Z.of_nat d) (Z.add (Z.mul (Z.opp x) alpha) (Z.mul y beta)), LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   elim H2. intro beta. intros.
(* Goal: LinComb (Z.of_nat d) x y *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   split with (- alpha)%Z. split with beta.
(* Goal: @eq Z (Z.of_nat d) (Z.add (Z.mul x (Z.opp alpha)) (Z.mul y beta)) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   rewrite H3.
(* Goal: @eq Z (Z.add (Z.opp (Z.mul x alpha)) (Z.mul y beta)) (Z.add (Z.mul (Z.opp alpha) x) (Z.mul y beta)) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   rewrite (Zmult_comm x). rewrite Zopp_mult_distr_l_reverse. rewrite Zopp_mult_distr_l_reverse.
(* Goal: @eq Z (Z.add (Z.opp (Z.mul x alpha)) (Z.mul y beta)) (Z.add (Z.opp (Z.mul x alpha)) (Z.mul y beta)) *)
(* Goal: Z.gt (Z.opp x) Z0 *)
(* Goal: gcd (Z.opp x) y d *)
   rewrite (Zmult_comm alpha). reflexivity.
(* Goal: gcd x y d *)
   apply Zopp_lt_gt_0. assumption. apply gcd_opp_l. assumption.
Qed.
