nouvel algorithme pour Zgcd (plus rapide) + un Qcompare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8989 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 975 insertions, 654 deletions

diff --git a/.depend.coq b/.depend.coq
index 949cc501cb..17de70f707 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -180,7 +180,7 @@ theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith_base.vo the
 theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Zeven.vo theories/ZArith/Zmin.vo theories/ZArith/Zmax.vo theories/ZArith/Zminmax.vo theories/ZArith/Zabs.vo theories/ZArith/Znat.vo theories/ZArith/auxiliary.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zbool.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
 theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/BinInt.vo theories/ZArith/Zeven.vo theories/ZArith/Zorder.vo theories/ZArith/Zcompare.vo theories/ZArith/ZArith_dec.vo theories/Bool/Sumbool.vo
 theories/ZArith/Zbinary.vo: theories/ZArith/Zbinary.v theories/Bool/Bvector.vo theories/ZArith/ZArith.vo theories/ZArith/Zpower.vo contrib/omega/Omega.vo
-theories/ZArith/Znumtheory.vo: theories/ZArith/Znumtheory.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdiv.vo
+theories/ZArith/Znumtheory.vo: theories/ZArith/Znumtheory.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdiv.vo theories/NArith/Ndigits.vo theories/Arith/Wf_nat.vo
 theories/ZArith/Int.vo: theories/ZArith/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo
 theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v theories/Relations/Relation_Definitions.vo
 theories/Lists/MonoList.vo: theories/Lists/MonoList.v theories/Arith/Le.vo
@@ -274,54 +274,6 @@ theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.
 theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
 theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
-theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
-theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
-theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
-theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
-theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
-theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplete.vo theories/Arith/Max.vo
-theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
-theories/Reals/Binomial.vo: theories/Reals/Binomial.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo
-theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
-theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binomial.vo
-theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
-theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
-theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo
-theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo
-theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo
-theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo
-theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
-theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo
-theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo
-theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo
-theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
-theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
-theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
-theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
-theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
-theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo
-theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo
-theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
-theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo
-theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
-theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo
-theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo
-theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
-theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo
-theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Arith/Arith.vo
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
@@ -332,6 +284,7 @@ theories/QArith/Qreduction.vo: theories/QArith/Qreduction.v theories/QArith/QAri
 theories/QArith/Qring.vo: theories/QArith/Qring.v contrib/ring/Ring.vo contrib/ring/Setoid_ring.vo theories/QArith/QArith_base.vo
 theories/QArith/Qreals.vo: theories/QArith/Qreals.v theories/Reals/Rbase.vo theories/QArith/QArith_base.vo
 theories/QArith/QArith.vo: theories/QArith/QArith.v theories/QArith/QArith_base.vo theories/QArith/Qring.vo theories/QArith/Qreduction.vo
+theories/QArith/Qcanon.vo: theories/QArith/Qcanon.v theories/QArith/QArith.vo theories/Logic/Eqdep_dec.vo contrib/field/Field.vo
 contrib/omega/OmegaLemmas.vo: contrib/omega/OmegaLemmas.v theories/ZArith/ZArith_base.vo
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/ZArith/Zhints.vo
 contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/Logic/Decidable.vo
@@ -353,7 +306,7 @@ contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v theories/Lists/List.
 contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo
 contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
 contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo
-contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo
+contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo
 contrib/subtac/Utils.vo: contrib/subtac/Utils.v
 contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theories/NArith/BinPos.vo
 contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo
diff --git a/Makefile b/Makefile
index 0d8c0745ac..ac37c8685e 100644
--- a/Makefile
+++ b/Makefile
@@ -874,7 +874,7 @@ ZARITHVO=\
 QARITHVO=\
  theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \
  theories/QArith/Qring.vo       theories/QArith/Qreals.vo \
- theories/QArith/QArith.vo
+ theories/QArith/QArith.vo	theories/QArith/Qcanon.vo 
 
 LISTSVO=\
  theories/Lists/MonoList.vo \
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 3b01b83d97..4354b5f95c 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -43,12 +43,48 @@ Notation Qge := (fun x y : Q => Qle y x).
 
 Infix "==" := Qeq (at level 70, no associativity) : Q_scope. 
 Infix "<" := Qlt : Q_scope.
+Infix ">" := Qgt : Q_scope.
 Infix "<=" := Qle : Q_scope.
-Infix ">" := Qgt : Q_scope. 
-Infix ">=" := Qge : Q_scope. 
+Infix ">=" := Qge : Q_scope.
 Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
 
-Hint Unfold Qeq Qle Qlt: qarith.
+(** Another approach : using Qcompare for defining order relations. *)
+
+Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z.
+Notation "p ?= q" := (Qcompare p q) : Q_scope.
+
+Lemma Qeq_alt : forall p q, (p == q) <-> (p ?= q) = Eq.
+Proof.
+unfold Qeq, Qcompare; intros; split; intros.
+rewrite H; apply Zcompare_refl.
+apply Zcompare_Eq_eq; auto.
+Qed.
+
+Lemma Qlt_alt : forall p q, (p<q) <-> (p?=q = Lt).
+Proof.
+unfold Qlt, Qcompare, Zlt; split; auto.
+Qed.
+
+Lemma Qgt_alt : forall p q, (p>q) <-> (p?=q = Gt).
+Proof.
+unfold Qlt, Qcompare, Zlt.
+intros; rewrite Zcompare_Gt_Lt_antisym; split; auto.
+Qed.
+
+Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).
+Proof.
+unfold Qle, Qcompare, Zle; split; auto.
+Qed.
+
+Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).
+Proof.
+unfold Qle, Qcompare, Zle.
+split; intros; swap H.
+rewrite Zcompare_Gt_Lt_antisym; auto.
+rewrite Zcompare_Gt_Lt_antisym in H0; auto.
+Qed.
+
+Hint Unfold Qeq Qlt Qle: qarith.
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
 (** Properties of equality. *)
@@ -236,6 +272,24 @@ apply Zmult_gt_0_lt_compat_l; auto with zarith.
 Open Scope Q_scope.
 Qed.
 
+
+Lemma Qcompare_egal_dec: forall n m p q : Q, 
+ (n<m -> p<q) -> (n==m -> p==q) -> (n>m -> p>q) -> ((n?=m) = (p?=q)).
+Proof.
+intros.
+do 2 rewrite Qeq_alt in H0.
+unfold Qeq, Qlt, Qcompare in *.
+apply Zcompare_egal_dec; auto.
+omega.
+Qed.
+
+
+Add Morphism Qcompare : Qcompare_comp.
+Proof.
+intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto.
+Qed.
+
+
 (** [0] and [1] are apart *)
 
 Lemma Q_apart_0_1 : ~ 1 == 0.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
new file mode 100644
index 0000000000..bc87e05d3c
--- /dev/null
+++ b/theories/QArith/Qcanon.v
@@ -0,0 +1,526 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import QArith.
+Require Import Eqdep_dec.
+
+(** [Qc] : A canonical representation of rational numbers. 
+   based on the setoid representation [Q]. *)
+
+Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }.
+
+Delimit Scope Qc_scope with Qc.
+Bind Scope Qc_scope with Qc.
+Arguments Scope Qcmake [Q_scope].
+Open Scope Qc_scope.
+
+Lemma Qred_identity : 
+ forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
+Proof.
+unfold Qred; intros (a,b); simpl.
+generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)).
+intros.
+rewrite H1 in H; clear H1.
+destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
+destruct H0.
+rewrite Zmult_1_l in H, H0.
+subst; simpl; auto.
+Qed.
+
+Lemma Qred_identity2 : 
+ forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z.
+Proof.
+unfold Qred; intros (a,b); simpl.
+generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)).
+intros.
+rewrite <- H; rewrite <- H in H1; clear H.
+destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
+injection H2; intros; clear H2.
+destruct H0.
+clear H0 H3.
+destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate.
+f_equal.
+apply Pmult_reg_r with bb.
+injection H2; intros. 
+rewrite <- H0.
+rewrite H; simpl; auto.
+elim H1; auto.
+Qed.
+
+Lemma Qred_iff : forall q:Q, Qred q = q <-> Zgcd (Qnum q) (QDen q) = 1%Z.
+Proof.
+split; intros.
+apply Qred_identity2; auto.
+apply Qred_identity; auto.
+Qed.
+
+
+Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q.
+Proof.
+intros; apply Qred_complete.
+apply Qred_correct.
+Qed.
+
+Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). 
+Arguments Scope Q2Qc [Q_scope].
+Notation " !! " := Q2Qc : Qc_scope.
+
+Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
+Proof.
+intros (q,proof_q) (q',proof_q').
+simpl.
+intros H.
+assert (H0:=Qred_complete _ _ H).
+assert (q = q') by congruence.
+subst q'.
+assert (proof_q = proof_q'). 
+ apply eq_proofs_unicity; auto; intros.
+ repeat decide equality.
+congruence.
+Qed.
+Hint Resolve Qc_is_canon.
+
+Notation " 0 " := (!!0) : Qc_scope.
+Notation " 1 " := (!!1) : Qc_scope.
+
+Definition Qcle (x y : Qc) := (x <= y)%Q.
+Definition Qclt (x y : Qc) := (x < y)%Q.
+Notation Qcgt := (fun x y : Qc => Qlt y x).
+Notation Qcge := (fun x y : Qc => Qle y x).
+Infix "<" := Qclt : Qc_scope.
+Infix "<=" := Qcle : Qc_scope.
+Infix ">" := Qcgt : Qc_scope. 
+Infix ">=" := Qcge : Qc_scope. 
+Notation "x <= y <= z" := (x<=y/\y<=z) : Qc_scope.
+
+Definition Qccompare (p q : Qc) := (Qcompare p q).
+Notation "p ?= q" := (Qccompare p q) : Qc_scope.
+
+Lemma Qceq_alt : forall p q, (p = q) <-> (p ?= q) = Eq.
+Proof.
+unfold Qccompare.
+intros; rewrite <- Qeq_alt.
+split; auto.
+intro H; rewrite H; auto with qarith.
+Qed.
+
+Lemma Qclt_alt : forall p q, (p<q) <-> (p?=q = Lt).
+Proof.
+intros; exact (Qlt_alt p q).
+Qed.
+
+Lemma Qcgt_alt : forall p q, (p>q) <-> (p?=q = Gt).
+Proof.
+intros; exact (Qgt_alt p q).
+Qed.
+
+Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).
+Proof.
+intros; exact (Qle_alt p q).
+Qed.
+
+Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).
+Proof.
+intros; exact (Qge_alt p q).
+Qed.
+
+(** equality on [Qc] is decidable: *)
+
+Theorem Qc_eq_dec : forall x y:Qc, {x=y} + {x<>y}.
+Proof.
+ intros.
+ destruct (Qeq_dec x y) as [H|H]; auto.
+ right; swap H; subst; auto with qarith.
+Defined. 
+
+(** The addition, multiplication and opposite are defined 
+   in the straightforward way: *)
+
+Definition Qcplus (x y : Qc) := !!(x+y).
+Infix "+" := Qcplus : Qc_scope.
+Definition Qcmult (x y : Qc) := !!(x*y).
+Infix "*" := Qcmult : Qc_scope.
+Definition Qcopp (x : Qc) := !!(-x).
+Notation "- x" := (Qcopp x) : Qc_scope.
+Definition Qcminus (x y : Qc) := x+-y.
+Infix "-" := Qcminus : Qc_scope.
+Definition Qcinv (x : Qc) := !!(/x).
+Notation "/ x" := (Qcinv x) : Qc_scope. 
+Definition Qcdiv (x y : Qc) := x*/y.
+Infix "/" := Qcdiv : Qc_scope. 
+
+(** [0] and [1] are apart *)
+
+Lemma Q_apart_0_1 : 1 <> 0.
+Proof.
+ unfold Q2Qc.
+ intros H; discriminate H.
+Qed.
+
+Ltac qc := match goal with 
+ | q:Qc |- _ => destruct q; qc 
+ | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct
+end.
+
+Opaque Qred.
+
+(** Addition is associative: *)
+
+Theorem Qcplus_assoc : forall x y z, x+(y+z)=(x+y)+z.
+Proof.
+ intros; qc; apply Qplus_assoc.
+Qed.
+
+(** [0] is a neutral element for addition: *)
+
+Lemma Qcplus_0_l : forall x, 0+x = x.
+Proof.
+ intros; qc; apply Qplus_0_l.
+Qed.
+
+Lemma Qcplus_0_r : forall x, x+0 = x.
+Proof.
+ intros; qc; apply Qplus_0_r.
+Qed. 
+
+(** Commutativity of addition: *)
+
+Theorem Qcplus_comm : forall x y, x+y = y+x.
+Proof.
+ intros; qc; apply Qplus_comm.
+Qed.
+
+(** Properties of [Qopp] *)
+
+Lemma Qcopp_involutive : forall q, - -q = q.
+Proof.
+ intros; qc; apply Qopp_involutive.
+Qed.
+
+Theorem Qcplus_opp_r : forall q, q+(-q) = 0.
+Proof.
+ intros; qc; apply Qplus_opp_r.
+Qed.
+
+(** Multiplication is associative: *)
+
+Theorem Qcmult_assoc : forall n m p, n*(m*p)=(n*m)*p.
+Proof.
+ intros; qc; apply Qmult_assoc.
+Qed.
+
+(** [1] is a neutral element for multiplication: *)
+
+Lemma Qcmult_1_l : forall n, 1*n = n.
+Proof.
+ intros; qc; apply Qmult_1_l.
+Qed.
+
+Theorem Qcmult_1_r : forall n, n*1=n.
+Proof.
+ intros; qc; apply Qmult_1_r.
+Qed.
+
+(** Commutativity of multiplication *)
+
+Theorem Qcmult_comm : forall x y, x*y=y*x.
+Proof.
+ intros; qc; apply Qmult_comm.
+Qed.
+
+(** Distributivity *)
+
+Theorem Qcmult_plus_distr_r : forall x y z, x*(y+z)=(x*y)+(x*z).
+Proof.
+ intros; qc; apply Qmult_plus_distr_r.
+Qed.
+
+Theorem Qcmult_plus_distr_l : forall x y z, (x+y)*z=(x*z)+(y*z).
+Proof.
+ intros; qc; apply Qmult_plus_distr_l.
+Qed.
+
+(** Integrality *)
+
+Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0.
+Proof.
+ intros.
+ destruct (Qmult_integral x y); try qc; auto.
+ injection H; clear H; intros.
+ rewrite <- (Qred_correct (x*y)).
+ rewrite <- (Qred_correct 0).
+ rewrite H; auto with qarith.
+Qed.
+
+Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x*y = 0 -> y = 0.
+Proof.
+ intros; destruct (Qcmult_integral _ _ H0); tauto.
+Qed. 
+
+(** Inverse and division. *) 
+
+Theorem Qcmult_inv_r : forall x, x<>0 -> x*(/x) = 1.
+Proof.
+ intros; qc; apply Qmult_inv_r; auto. 
+Qed.
+
+Theorem Qcmult_inv_l : forall x, x<>0 -> (/x)*x = 1.
+Proof.
+ intros.
+ rewrite Qcmult_comm.
+ apply Qcmult_inv_r; auto.
+Qed.
+
+Lemma Qcinv_mult_distr : forall p q, / (p * q) = /p * /q.
+Proof.
+ intros; qc; apply Qinv_mult_distr.
+Qed.
+
+Theorem Qcdiv_mult_l : forall x y, y<>0 -> (x*y)/y = x.
+Proof.
+ unfold Qcdiv.
+ intros.
+ rewrite <- Qcmult_assoc.
+ rewrite Qcmult_inv_r; auto.
+ apply Qcmult_1_r.
+Qed.
+
+Theorem Qcmult_div_r : forall x y, ~ y = 0 -> y*(x/y) = x.
+Proof.
+ unfold Qcdiv.
+ intros.
+ rewrite Qcmult_assoc.
+ rewrite Qcmult_comm.
+ rewrite Qcmult_assoc.
+ rewrite Qcmult_inv_l; auto.
+ apply Qcmult_1_l.
+Qed.
+
+(** Properties of order upon Q. *)
+
+Lemma Qcle_refl : forall x, x<=x.
+Proof.
+unfold Qcle; intros; simpl; apply Qle_refl.
+Qed.
+
+Lemma Qcle_antisym : forall x y, x<=y -> y<=x -> x=y.
+Proof.
+unfold Qcle; intros; simpl in *.
+apply Qc_is_canon; apply Qle_antisym; auto.
+Qed.
+
+Lemma Qcle_trans : forall x y z, x<=y -> y<=z -> x<=z.
+Proof.
+unfold Qcle; intros; eapply Qle_trans; eauto.
+Qed.
+
+Lemma Qclt_not_eq : forall x y, x<y -> x<>y.
+Proof.
+unfold Qclt; intros; simpl in *.
+intro; destruct (Qlt_not_eq _ _ H).
+subst; auto with qarith.
+Qed.
+
+(** Large = strict or equal *)
+
+Lemma Qclt_le_weak : forall x y, x<y -> x<=y.
+Proof.
+unfold Qcle, Qclt; intros; apply Qlt_le_weak; auto.
+Qed.
+
+Lemma Qcle_lt_trans : forall x y z, x<=y -> y<z -> x<z.
+Proof.
+unfold Qcle, Qclt; intros; eapply Qle_lt_trans; eauto.
+Qed.
+
+Lemma Qclt_le_trans : forall x y z, x<y -> y<=z -> x<z.
+Proof.
+unfold Qcle, Qclt; intros; eapply Qlt_le_trans; eauto.
+Qed.
+
+Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z.
+Proof.
+unfold Qclt; intros; eapply Qlt_trans; eauto.
+Qed.
+
+(** [x<y] iff [~(y<=x)] *)
+
+Lemma Qcnot_lt_le : forall x y, ~ x<y -> y<=x.
+Proof.
+unfold Qcle, Qclt; intros; apply Qnot_lt_le; auto.
+Qed.
+
+Lemma Qcnot_le_lt : forall x y, ~ x<=y -> y<x.
+Proof.
+unfold Qcle, Qclt; intros; apply Qnot_le_lt; auto.
+Qed.
+
+Lemma Qclt_not_le : forall x y, x<y -> ~ y<=x.
+Proof.
+unfold Qcle, Qclt; intros; apply Qlt_not_le; auto.
+Qed.
+
+Lemma Qcle_not_lt : forall x y, x<=y -> ~ y<x.
+Proof.
+unfold Qcle, Qclt; intros; apply Qle_not_lt; auto.
+Qed.
+
+Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.
+Proof.
+unfold Qcle, Qclt; intros; apply Qle_lt_or_eq; auto.
+Qed.
+
+(** Some decidability results about orders. *)
+
+Lemma Qc_dec : forall x y, {x<y} + {y<x} + {x=y}.
+Proof.
+unfold Qclt, Qcle; intros.
+destruct (Q_dec x y) as [H|H].
+left; auto.
+right; apply Qc_is_canon; auto.
+Defined.
+
+Lemma Qclt_le_dec : forall x y, {x<y} + {y<=x}.
+Proof.
+unfold Qclt, Qcle; intros; apply Qlt_le_dec; auto.
+Defined.
+
+(** Compatibility of operations with respect to order. *)
+
+Lemma Qcopp_le_compat : forall p q, p<=q -> -q <= -p.
+Proof.
+unfold Qcle, Qcopp; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qopp_le_compat; auto.
+Qed.
+
+Lemma Qcle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
+Proof.
+unfold Qcle, Qcminus; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qle_minus_iff; auto.
+Qed.
+
+Lemma Qclt_minus_iff : forall p q, p < q <-> 0 < q+-p.
+Proof.
+unfold Qclt, Qcplus, Qcopp; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qlt_minus_iff; auto.
+Qed.
+
+Lemma Qcplus_le_compat :
+ forall x y z t, x<=y -> z<=t -> x+z <= y+t.
+Proof.
+unfold Qcplus, Qcle; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qplus_le_compat; auto.
+Qed.
+
+Lemma Qcmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.
+Proof.
+unfold Qcmult, Qcle; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qmult_le_compat_r; auto.
+Qed.
+
+Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 <  z  -> x*z <= y*z -> x <= y.
+Proof.
+unfold Qcmult, Qcle, Qclt; intros; simpl in *.
+repeat progress rewrite Qred_correct in * |-. 
+eapply Qmult_lt_0_le_reg_r; eauto.
+Qed.
+
+Lemma Qcmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.
+Proof.
+unfold Qcmult, Qclt; intros; simpl in *.
+repeat progress rewrite Qred_correct in *. 
+eapply Qmult_lt_compat_r; eauto.
+Qed.
+
+(** Rational to the n-th power *)
+
+Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc := 
+ match n with 
+  | O => 1
+  | S n => q * (Qcpower q n)
+ end. 
+
+Notation " q ^ n " := (Qcpower q n) : Qc_scope.
+
+Lemma Qcpower_1 : forall n, 1^n = 1.
+Proof.
+induction n; simpl; auto with qarith.
+rewrite IHn; auto with qarith.
+Qed.
+
+Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.
+Proof.
+destruct n; simpl.
+destruct 1; auto.
+intros. 
+apply Qc_is_canon.
+simpl.
+compute; auto.
+Qed.
+
+Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n.
+Proof.
+induction n; simpl; auto with qarith.
+intros; compute; intro; discriminate.
+intros.
+apply Qcle_trans with (0*(p^n)).
+compute; intro; discriminate.
+apply Qcmult_le_compat_r; auto.
+Qed.
+
+(** And now everything is easier concerning tactics: *)
+
+(** A ring tactic for rational numbers *)
+
+Definition Qc_eq_bool (x y : Qc) :=
+  if Qc_eq_dec x y then true else false.
+
+Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y.
+intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto.
+intros _ H; inversion H.
+Qed.
+
+Definition Qcrt : Ring_Theory Qcplus Qcmult 1 0 Qcopp Qc_eq_bool.
+Proof.
+constructor.
+exact Qcplus_comm.
+exact Qcplus_assoc.
+exact Qcmult_comm.
+exact Qcmult_assoc.
+exact Qcplus_0_l.
+exact Qcmult_1_l.
+exact Qcplus_opp_r.
+exact Qcmult_plus_distr_l.
+unfold Is_true; intros x y; generalize (Qc_eq_bool_correct x y);
+ case (Qc_eq_bool x y); auto.
+Qed.
+
+Add Ring Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcrt [ Qcmake ].
+
+(** A field tactic for rational numbers *)
+
+Require Import Field.
+
+Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l
+ with div:=Qcdiv.
+
+Example test_field : forall x y : Qc, y<>0 -> (x/y)*y = x.
+intros.
+field.
+auto.
+Qed.
+
+
+
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index b818f744ff..41e0d9a456 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -32,65 +32,17 @@ Proof.
  simple destruct z; simpl in |- *; auto; intros; elim H; auto.
 Qed.
 
-(** A simple cancelation by powers of two *)
-
-Fixpoint Pfactor_twos (p p':positive) {struct p} : (positive*positive) := 
- match p, p' with 
-  | xO p, xO p' => Pfactor_twos p p'
-  | _, _ => (p,p')
- end.
-
-Definition Qfactor_twos (q:Q) := 
- let (p,q) := q in 
- match p with 
-   | Z0 => 0
-   | Zpos p => let (p,q) := Pfactor_twos p q in (Zpos p)#q
-   | Zneg p => let (p,q) := Pfactor_twos p q in (Zneg p)#q
- end.
-
-Lemma Pfactor_twos_correct : forall p p', 
-   (p*(snd (Pfactor_twos p p')))%positive = 
-   (p'*(fst (Pfactor_twos p p')))%positive.
-Proof.
-induction p; intros.
-simpl snd; simpl fst; rewrite Pmult_comm; auto.
-destruct p'.
-simpl snd; simpl fst; rewrite Pmult_comm; auto.
-simpl; f_equal; auto.
-simpl snd; simpl fst; rewrite Pmult_comm; auto.
-simpl snd; simpl fst; rewrite Pmult_comm; auto.
-Qed.
-
-Lemma Qfactor_twos_correct : forall q, Qfactor_twos q == q.
-Proof.
-intros (p,q).
-destruct p.
-red; simpl; auto.
-simpl.
-generalize (Pfactor_twos_correct p q); destruct (Pfactor_twos p q).
-red; simpl.
-intros; f_equal.
-rewrite H; apply Pmult_comm.
-simpl.
-generalize (Pfactor_twos_correct p q); destruct (Pfactor_twos p q).
-red; simpl.
-intros; f_equal.
-rewrite H; apply Pmult_comm.
-Qed.
-Hint Resolve Qfactor_twos_correct.
-
 (** Simplification of fractions using [Zgcd].
   This version can compute within Coq. *)
 
 Definition Qred (q:Q) := 
-  let (q1,q2) := Qfactor_twos q in 
-  let (r1,r2) := snd (Zggcd q1 (Zpos q2)) in r1#(Z2P r2).
+  let (q1,q2) := q in 
+  let (r1,r2) := snd (Zggcd q1 ('q2)) 
+  in r1#(Z2P r2).
 
 Lemma Qred_correct : forall q, (Qred q) == q.
 Proof.
-intros; apply Qeq_trans with (Qfactor_twos q); auto.
-unfold Qred.
-destruct (Qfactor_twos q) as (n,d); red; simpl.
+unfold Qred, Qeq; intros (n,d); simpl.
 generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d)) 
   (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)).
 destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl.
@@ -112,16 +64,8 @@ Qed.
 
 Lemma Qred_complete : forall p q,  p==q -> Qred p = Qred q.
 Proof.
-intros.
-assert (Qfactor_twos p == Qfactor_twos q).
- apply Qeq_trans with p; auto.
- apply Qeq_trans with q; auto.
- symmetry; auto.
-clear H.
-unfold Qred.
-destruct (Qfactor_twos p) as (a,b); 
-destruct (Qfactor_twos q) as (c,d); clear p q.
-unfold Qeq in *; simpl in *.
+intros (a,b) (c,d).
+unfold Qred, Qeq in *; simpl in *.
 Open Scope Z_scope.
 generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) 
  (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)).
@@ -198,47 +142,6 @@ rewrite (Qred_correct q); auto.
 rewrite (Qred_correct q'); auto.
 Qed.
 
-(** Another version, dedicated to extraction *)
-
-Definition Qred_extr (q : Q) :=
-  let (q1, q2) := Qfactor_twos q in
-  let (p,_) := Zggcd_spec_pos (Zpos q2) (Zle_0_pos q2) q1 in  
-  let (r2,r1) := snd p in r1#(Z2P r2).
-
-Lemma Qred_extr_Qred : forall q, Qred_extr q = Qred q.
-Proof.
-unfold Qred, Qred_extr.
-intro q; destruct (Qfactor_twos q) as (n,p); clear q.
-Open Scope Z_scope.
-destruct (Zggcd_spec_pos (' p) (Zle_0_pos p) n) as ((g,(pp,nn)),H).
-generalize (H (Zle_0_pos p)); clear H; intros (Hg1,(Hg2,(Hg4,Hg3))).
-simpl.
-generalize (Zggcd_gcd n ('p)) (Zgcd_is_gcd n ('p)) 
- (Zgcd_is_pos n ('p)) (Zggcd_correct_divisors n ('p)).
-destruct (Zggcd n (Zpos p)) as (g',(nn',pp')); simpl.
-intro H; rewrite <- H; clear H.
-intros Hg'1 Hg'2 (Hg'3,Hg'4).
-assert (g<>0).
- intro; subst g; discriminate.
-destruct (Zis_gcd_uniqueness_apart_sign n ('p) g g'); auto.
-apply Zis_gcd_sym; auto.
-subst g'.
-f_equal.
-apply Zmult_reg_l with g; auto; congruence.
-f_equal.
-apply Zmult_reg_l with g; auto; congruence.
-elimtype False; omega.
-Open Scope Q_scope.
-Qed.
-
-Add Morphism Qred_extr : Qred_extr_comp. 
-Proof.
-intros q q' H.
-do 2 rewrite Qred_extr_Qred.
-rewrite (Qred_correct q); auto.
-rewrite (Qred_correct q'); auto.
-Qed.
-
 Definition Qplus' (p q : Q) := Qred (Qplus p q).
 Definition Qmult' (p q : Q) := Qred (Qmult p q). 
 
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 3a610226e2..d61cc84bcc 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -12,15 +12,17 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
+Require Import Ndigits.
+Require Import Wf_nat.
 Open Local Scope Z_scope.
 
 (** This file contains some notions of number theory upon Z numbers: 
      - a divisibility predicate [Zdivide]
      - a gcd predicate [gcd]
      - Euclid algorithm [euclid]
-     - an efficient [Zgcd] function 
      - a relatively prime predicate [rel_prime]
      - a prime predicate [prime]
+     - an efficient [Zgcd] function 
 *)
 
 (** * Divisibility *)
@@ -215,6 +217,16 @@ Proof.
 constructor; auto with zarith.
 Qed.
 
+Lemma Zis_gcd_1 : forall a, Zis_gcd a 1 1.
+Proof.
+constructor; auto with zarith.
+Qed.
+
+Lemma Zis_gcd_refl : forall a, Zis_gcd a a a.
+Proof.
+constructor; auto with zarith.
+Qed.
+
 Lemma Zis_gcd_minus : forall a b d:Z, Zis_gcd a (- b) d -> Zis_gcd b a d.
 Proof.
 simple induction 1; constructor; intuition.
@@ -225,6 +237,14 @@ Proof.
 simple induction 1; constructor; intuition.
 Qed.
 
+Lemma Zis_gcd_0_abs : forall a:Z, Zis_gcd 0 a (Zabs a).
+Proof.
+intros a.
+apply Zabs_ind.
+intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto.
+intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto.
+Qed.
+
 Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.
 
 (** * Extended Euclid algorithm. *)
@@ -366,478 +386,8 @@ replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)).
 rewrite H6; rewrite H7; ring.
 ring.
 Qed.
-
-Lemma Zis_gcd_0_abs : forall b, 
- Zis_gcd 0 b (Zabs b) /\ Zabs b >= 0 /\ 0 = Zabs b * 0 /\ b = Zabs b * Zsgn b.
-Proof.
-intro b.
-elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)).
-intros H0; split.
-apply Zabs_ind.
-intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto.
-intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto.
-repeat split; auto with zarith.
-symmetry; apply Zabs_Zsgn.
-
-intros H0; rewrite <- H0.
-rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *.
-split; [ apply Zis_gcd_0 | idtac ]; auto with zarith.
-Qed.
   
 
-(** We could obtain a [Zgcd] function via [euclid]. But we propose 
-  here a more direct version of a [Zgcd], that can compute within Coq.
-  For that, we use an explicit measure in [nat], and we proved later
-  that using [2(d+1)] is enough, where  [d] is the number of binary digits 
-  of the first argument. *)
-
-Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b => 
- match n with 
-  | O => 1 (* arbitrary, since n should be big enough *)
-  | S n => match a with 
-     | Z0 => Zabs b
-     | Zpos _ => Zgcdn n (Zmod b a) a
-     | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a)
-     end
-   end.
-
-(* For technical reason, we don't use [Ndigit.Psize] but this 
-   ad-hoc version: [Psize p = S (Psiz p)]. *)
-
-Fixpoint Psiz (p:positive) : nat := 
-  match p with 
-    | xH => O
-    | xI p => S (Psiz p) 
-    | xO p => S (Psiz p)
-  end.
-
-Definition Zgcd_bound (a:Z) := match a with 
- | Z0 => S O
- | Zpos p => let n := Psiz p in S (S (n+n))
- | Zneg p => let n := Psiz p in S (S (n+n))
-end.
-
-Definition Zgcd a b := Zgcdn (Zgcd_bound a) a b.
-
-(** A first obvious fact : [Zgcd a b] is positive. *)
-
-Lemma Zgcdn_is_pos : forall n a b, 
-  0 <= Zgcdn n a b.
-Proof.
-induction n.
-simpl; auto with zarith.
-destruct a; simpl; intros; auto with zarith; auto.
-Qed.
-
-Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b.
-Proof.
-intros; unfold Zgcd; apply Zgcdn_is_pos; auto.
-Qed.
-
-(** We now prove that Zgcd is indeed a gcd. *)
-
-(** 1) We prove a weaker & easier bound. *)
-
-Lemma Zgcdn_linear_bound : forall n a b, 
- Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b).
-Proof.
-induction n.
-simpl; intros.
-elimtype False; generalize (Zabs_pos a); omega.
-destruct a; intros; simpl; 
- [ generalize (Zis_gcd_0_abs b); intuition | | ]; 
- unfold Zmod; 
- generalize (Z_div_mod b (Zpos p) (refl_equal Gt));
- destruct (Zdiv_eucl b (Zpos p)) as (q,r);
- intros (H0,H1); 
- rewrite inj_S in H; simpl Zabs in H; 
- assert (H2: Zabs r < Z_of_nat n) by (rewrite Zabs_eq; auto with zarith);  
- assert (IH:=IHn r (Zpos p) H2); clear IHn; 
- simpl in IH |- *; 
- rewrite H0.
- apply Zis_gcd_for_euclid2; auto.
- apply Zis_gcd_minus; apply Zis_gcd_sym.
- apply Zis_gcd_for_euclid2; auto.
-Qed.
-
-(** 2) For Euclid's algorithm, the worst-case situation corresponds 
-     to Fibonacci numbers. Let's define them: *)
-
-Fixpoint fibonacci (n:nat) : Z := 
- match n with 
-   | O => 1
-   | S O => 1
-   | S (S n as p) => fibonacci p + fibonacci n 
- end.
-
-Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
-Proof.
-cut (forall N n, (n<N)%nat -> 0<=fibonacci n).
-eauto.
-induction N.
-inversion 1.
-intros.
-destruct n.
-simpl; auto with zarith.
-destruct n.
-simpl; auto with zarith.
-change (0 <= fibonacci (S n) + fibonacci n).
-generalize (IHN n) (IHN (S n)); omega.
-Qed.
-
-Lemma fibonacci_incr : 
- forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m.
-Proof.
-induction 1.
-auto with zarith.
-apply Zle_trans with (fibonacci m); auto.
-clear.
-destruct m.
-simpl; auto with zarith.
-change (fibonacci (S m) <= fibonacci (S m)+fibonacci m).
-generalize (fibonacci_pos m); omega.
-Qed.
-
-(** 3) We prove that fibonacci numbers are indeed worst-case: 
-   for a given number [n], if we reach a conclusion about [gcd(a,b)] in 
-   exactly [n+1] loops, then [fibonacci (n+1)<=a /\ fibonacci(n+2)<=b] *)
-
-Lemma Zgcdn_worst_is_fibonacci : forall n a b, 
- 0 < a < b -> 
- Zis_gcd a b (Zgcdn (S n) a b) -> 
- Zgcdn n a b <> Zgcdn (S n) a b -> 
- fibonacci (S n) <= a /\ 
- fibonacci (S (S n)) <= b.
-Proof.
-induction n.
-simpl; intros.
-destruct a; omega.
-intros.
-destruct a; [simpl in *; omega| | destruct H; discriminate].
-revert H1; revert H0.
-set (m:=S n) in *; (assert (m=S n) by auto); clearbody m.
-pattern m at 2; rewrite H0.
-simpl Zgcdn.
-unfold Zmod; generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-intros (H1,H2).
-destruct H2.
-destruct (Zle_lt_or_eq _ _ H2).
-generalize (IHn _ _ (conj H4 H3)).
-intros H5 H6 H7. 
-replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto.
-assert (r = Zpos p * (-q) + b) by (rewrite H1; ring).
-destruct H5; auto.
-pattern r at 1; rewrite H8.
-apply Zis_gcd_sym.
-apply Zis_gcd_for_euclid2; auto.
-apply Zis_gcd_sym; auto.
-split; auto.
-rewrite H1.
-apply Zplus_le_compat; auto.
-apply Zle_trans with (Zpos p * 1); auto.
-ring (Zpos p * 1); auto.
-apply Zmult_le_compat_l.
-destruct q.
-omega.
-assert (0 < Zpos p0) by (compute; auto).
-omega.
-assert (Zpos p * Zneg p0 < 0) by (compute; auto).
-omega. 
-compute; intros; discriminate.
-(* r=0 *)
-subst r.
-simpl; rewrite H0.
-intros.
-simpl in H4.
-simpl in H5.
-destruct n.
-simpl in H5.
-simpl.
-omega.
-simpl in H5.
-elim H5; auto.
-Qed.
-
-(** 3b) We reformulate the previous result in a more positive way. *)
-
-Lemma Zgcdn_ok_before_fibonacci : forall n a b, 
- 0 < a < b -> a < fibonacci (S n) ->
- Zis_gcd a b (Zgcdn n a b).
-Proof.
-destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate].
-cut (forall k n b, 
-         k = (S (nat_of_P p) - n)%nat -> 
-         0 < Zpos p < b -> Zpos p < fibonacci (S n) -> 
-         Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)).
-destruct 2; eauto.
-clear n; induction k. 
-intros.
-assert (nat_of_P p < n)%nat by omega.
-apply Zgcdn_linear_bound. 
-simpl.
-generalize (inj_le _ _ H2).
-rewrite inj_S.
-rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto.
-omega.
-intros.
-generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros.
-assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)).
- apply IHk; auto.
- omega.
- replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto.
- generalize (fibonacci_pos n); omega.
-replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto.
-generalize (H2 H3); clear H2 H3; omega.
-Qed.
-
-(** 4) The proposed bound leads to a fibonacci number that is big enough. *)
-
-Lemma Zgcd_bound_fibonacci : 
-  forall a, 0 < a -> a < fibonacci (Zgcd_bound a).
-Proof.
-destruct a; [omega| | intro H; discriminate].
-intros _.
-induction p.
-simpl Zgcd_bound in *.
-rewrite Zpos_xI.
-rewrite plus_comm; simpl plus.
-set (n:=S (Psiz p+Psiz p)) in *.
-change (2*Zpos p+1 < 
- fibonacci (S n) + fibonacci n + fibonacci (S n)).
-generalize (fibonacci_pos n).
-omega.
-simpl Zgcd_bound in *.
-rewrite Zpos_xO.
-rewrite plus_comm; simpl plus.
-set (n:= S (Psiz p +Psiz p)) in *.
-change (2*Zpos p < 
- fibonacci (S n) + fibonacci n + fibonacci (S n)).
-generalize (fibonacci_pos n).
-omega.
-simpl; auto with zarith.
-Qed.
-
-(* 5) the end: we glue everything together and take care of 
-   situations not corresponding to [0<a<b]. *)
-
-Lemma Zgcd_is_gcd : 
-  forall a b, Zis_gcd a b (Zgcd a b).
-Proof.
-unfold Zgcd; destruct a; intros.
-simpl; generalize (Zis_gcd_0_abs b); intuition.
-(*Zpos*)
-generalize (Zgcd_bound_fibonacci (Zpos p)).
-simpl Zgcd_bound.
-set (n:=S (Psiz p+Psiz p)); (assert (n=S (Psiz p+Psiz p)) by auto); clearbody n.
-simpl Zgcdn.
-unfold Zmod.
-generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-intros (H1,H2) H3.
-rewrite H1.
-apply Zis_gcd_for_euclid2.
-destruct H2.
-destruct (Zle_lt_or_eq _ _ H0).
-apply Zgcdn_ok_before_fibonacci; auto; omega.
-subst r n; simpl.
-apply Zis_gcd_sym; apply Zis_gcd_0.
-(*Zneg*)
-generalize (Zgcd_bound_fibonacci (Zpos p)).
-simpl Zgcd_bound.
-set (n:=S (Psiz p+Psiz p)); (assert (n=S (Psiz p+Psiz p)) by auto); clearbody n.
-simpl Zgcdn.
-unfold Zmod.
-generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-intros (H1,H2) H3.
-rewrite H1.
-apply Zis_gcd_minus.
-apply Zis_gcd_sym.
-apply Zis_gcd_for_euclid2.
-destruct H2.
-destruct (Zle_lt_or_eq _ _ H0).
-apply Zgcdn_ok_before_fibonacci; auto; omega.
-subst r n; simpl.
-apply Zis_gcd_sym; apply Zis_gcd_0.
-Qed.
-
-(** A generalized gcd: it additionnally keeps track of the divisors. *)
-
-Fixpoint Zggcdn (n:nat) : Z -> Z -> (Z*(Z*Z)) := fun a b => 
- match n with 
-  | O => (1,(a,b))   (*(Zabs b,(0,Zsgn b))*)
-  | S n => match a with 
-     | Z0 => (Zabs b,(0,Zsgn b))
-     | Zpos _ => 
-               let (q,r) := Zdiv_eucl b a in   (* b = q*a+r *)
-               let (g,p) := Zggcdn n r a in 
-               let (rr,aa) := p in        (* r = g *rr /\ a = g * aa *)
-               (g,(aa,q*aa+rr))
-     | Zneg a => 
-               let (q,r) := Zdiv_eucl b (Zpos a) in  (* b = q*(-a)+r *)
-               let (g,p) := Zggcdn n r (Zpos a) in 
-               let (rr,aa) := p in         (* r = g*rr /\ (-a) = g * aa *)  
-               (g,(-aa,q*aa+rr))
-     end
-   end.
-
-Definition Zggcd a b : Z * (Z * Z) := Zggcdn (Zgcd_bound a) a b.
-
-(** The first component of [Zggcd] is [Zgcd] *) 
-
-Lemma Zggcdn_gcdn : forall n a b, 
- fst (Zggcdn n a b) = Zgcdn n a b.
-Proof.
-induction n; simpl; auto.
-destruct a; unfold Zmod; simpl; intros; auto; 
- destruct (Zdiv_eucl b (Zpos p)) as (q,r); 
- rewrite <- IHn; 
- destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)); simpl; auto.
-Qed.
-
-Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b.
-Proof.
-intros; unfold Zggcd, Zgcd; apply Zggcdn_gcdn; auto.
-Qed.
-
-(** [Zggcd] always returns divisors that are coherent with its 
- first output. *)
-
-Lemma Zggcdn_correct_divisors : forall n a b, 
-  let (g,p) := Zggcdn n a b in 
-  let (aa,bb):=p in 
-  a=g*aa /\ b=g*bb.
-Proof.
-induction n.
-simpl.
-split; [destruct a|destruct b]; auto.
-intros.
-simpl.
-destruct a.
-rewrite Zmult_comm; simpl.
-split; auto.
-symmetry; apply Zabs_Zsgn.
-generalize (Z_div_mod b (Zpos p)); 
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-generalize (IHn r (Zpos p)); 
-destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)).
-intuition.
-destruct H0.
-compute; auto.
-rewrite H; rewrite H1; rewrite H2; ring.
-generalize (Z_div_mod b (Zpos p)); 
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-destruct 1.
-compute; auto.
-generalize (IHn r (Zpos p)); 
-destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)).
-intuition.
-destruct H0.
-replace (Zneg p) with (-Zpos p) by compute; auto.
-rewrite H4; ring.
-rewrite H; rewrite H4; rewrite H0; ring.
-Qed.
-
-Lemma Zggcd_correct_divisors : forall a b, 
-  let (g,p) := Zggcd a b in 
-  let (aa,bb):=p in 
-  a=g*aa /\ b=g*bb.
-Proof.
-unfold Zggcd; intros; apply Zggcdn_correct_divisors; auto.
-Qed.
- 
-(** Due to the use of an explicit measure, the extraction of [Zgcd] 
-  isn't optimal. We propose here another version [Zgcd_spec] that 
-  doesn't suffer from this problem (but doesn't compute in Coq). *)
-
-Definition Zgcd_spec_pos :
-  forall a:Z,
-    0 <= a -> forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}.
-Proof.
-intros a Ha.
-apply
- (Zlt_0_rec
-    (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}));
- try assumption.
-intro x; case x.
-intros _ _ b; exists (Zabs b).
-generalize (Zis_gcd_0_abs b); intuition.
-  
-intros p Hrec _ b.
-generalize (Z_div_mod b (Zpos p)).
-case (Zdiv_eucl b (Zpos p)); intros q r Hqr.
-elim Hqr; clear Hqr; intros; auto with zarith.
-elim (Hrec r H0 (Zpos p)); intros g Hgkl.
-inversion_clear H0.
-elim (Hgkl H1); clear Hgkl; intros H3 H4.
-exists g; intros.
-split; auto.
-rewrite H.
-apply Zis_gcd_for_euclid2; auto.
-
-intros p _ H b.
-elim H; auto.
-Defined.
-
-Definition Zgcd_spec : forall a b:Z, {g : Z | Zis_gcd a b g /\ g >= 0}.
-Proof.
-intros a; case (Z_gt_le_dec 0 a).
-intros; assert (0 <= - a).
-omega.
-elim (Zgcd_spec_pos (- a) H b); intros g Hgkl.
-exists g.
-intuition.
-intros Ha b; elim (Zgcd_spec_pos a Ha b); intros g; exists g; intuition.
-Defined.
-
-(** A last version aimed at extraction that also returns the divisors. *)
-
-Definition Zggcd_spec_pos :
-  forall a:Z,
-    0 <= a -> forall b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in 
-                                       0 <= a -> Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}.
-Proof.
-intros a Ha.
-pattern a; apply Zlt_0_rec; try assumption.
-intro x; case x.
-intros _ _ b; exists (Zabs b,(0,Zsgn b)).
-intros _; apply Zis_gcd_0_abs.
-  
-intros p Hrec _ b.
-generalize (Z_div_mod b (Zpos p)).
-case (Zdiv_eucl b (Zpos p)); intros q r Hqr.
-elim Hqr; clear Hqr; intros; auto with zarith.
-destruct (Hrec r H0 (Zpos p)) as ((g,(rr,pp)),Hgkl).
-destruct H0.
-destruct (Hgkl H0) as (H3,(H4,(H5,H6))).
-exists (g,(pp,pp*q+rr)); intros.
-split; auto.
-rewrite H.
-apply Zis_gcd_for_euclid2; auto.
-repeat split; auto.
-rewrite H; rewrite H6; rewrite H5; ring.
-
-intros p _ H b.
-elim H; auto.
-Defined.
-
-Definition Zggcd_spec : 
- forall a b:Z, {p : Z*(Z*Z) |  let (g,p):=p in let (aa,bb):=p in 
-                                          Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}.
-Proof.
-intros a; case (Z_gt_le_dec 0 a).
-intros; assert (0 <= - a).
-omega.
-destruct (Zggcd_spec_pos (- a) H b) as ((g,(aa,bb)),Hgkl).
-exists (g,(-aa,bb)).
-intuition.
-rewrite <- Zopp_mult_distr_r.
-rewrite <- H2; auto with zarith.
-intros Ha b; elim (Zggcd_spec_pos a Ha b); intros p; exists p.
- repeat destruct p; intuition.
-Defined.
-
 (** * Relative primality *)
 
 Definition rel_prime (a b:Z) : Prop := Zis_gcd a b 1.
@@ -920,32 +470,25 @@ assert (g <> 0).
  elim H4; intros.
  rewrite H2 in H6; subst b; omega.
 unfold rel_prime in |- *.
-elim (Zgcd_spec (a / g) (b / g)); intros g' [H3 H4].
-assert (H5 := Zis_gcd_mult _ _ g _ H3).
-rewrite <- Z_div_exact_2 in H5; auto with zarith.
-rewrite <- Z_div_exact_2 in H5; auto with zarith.
-elim (Zis_gcd_uniqueness_apart_sign _ _ _ _ H1 H5).
-intros; rewrite (Zmult_reg_l 1 g' g); auto with zarith.
-intros; rewrite (Zmult_reg_l 1 (- g') g); auto with zarith.
-pattern g at 1 in |- *; rewrite H6; ring.
-
-elim H1; intros.
-elim H7; intros.
-rewrite H9.
-replace (q * g) with (0 + q * g).
-rewrite Z_mod_plus.
-compute in |- *; auto.
-omega.
-ring.
-
-elim H1; intros.
-elim H6; intros.
-rewrite H9.
-replace (q * g) with (0 + q * g).
-rewrite Z_mod_plus.
-compute in |- *; auto.
-omega.
-ring.
+destruct H1.
+destruct H1 as (a',H1).
+destruct H3 as (b',H3).
+replace (a/g) with a'; 
+ [|rewrite H1; rewrite Z_div_mult; auto with zarith].
+replace (b/g) with b'; 
+ [|rewrite H3; rewrite Z_div_mult; auto with zarith].
+constructor.
+exists a'; auto with zarith.
+exists b'; auto with zarith.
+intros x (xa,H5) (xb,H6).
+destruct (H4 (x*g)).
+exists xa; rewrite Zmult_assoc; rewrite <- H5; auto.
+exists xb; rewrite Zmult_assoc; rewrite <- H6; auto.
+replace g with (1*g) in H7; auto with zarith.
+do 2 rewrite Zmult_assoc in H7.
+generalize (Zmult_reg_r _ _ _ H2 H7); clear H7; intros.
+rewrite Zmult_1_r in H7.
+exists q; auto with zarith.
 Qed.
 
 (** * Primality *)
@@ -1045,3 +588,345 @@ case (Zdivide_dec p a); intuition.
 right; apply Gauss with a; auto with zarith.
 Qed.
 
+
+(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose 
+  here a binary version of [Zgcd], faster and executable within Coq.
+
+   Algorithm: 
+
+   gcd 0 b = b
+   gcd a 0 = a
+   gcd (2a) (2b) = 2(gcd a b)
+   gcd (2a+1) (2b) = gcd (2a+1) b
+   gcd (2a) (2b+1) = gcd a (2b+1)
+   gcd (2a+1) (2b+1) = gcd (b-a) (2*a+1)
+                    or gcd (a-b) (2*b+1), depending on whether a<b 
+*)   
+
+Open Scope positive_scope.
+
+Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive := 
+ match n with 
+  | O => 1
+  | S n => 
+     match a,b with 
+       | xH, _ => 1 
+       | _, xH => 1
+       | xO a, xO b => xO (Pgcdn n a b)
+       | a, xO b => Pgcdn n a b
+       | xO a, b => Pgcdn n a b
+       | xI a', xI b' => match Pcompare a' b' Eq with 
+           | Eq => a
+           | Lt => Pgcdn  n (b'-a') a
+           | Gt => Pgcdn n (a'-b') b
+         end
+     end
+  end.
+
+Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := 
+ match n with 
+  | O => (1,(a,b))
+  | S n => 
+     match a,b with 
+       | xH, b => (1,(1,b)) 
+       | a, xH => (1,(a,1))
+       | xO a, xO b => 
+             let (g,p) := Pggcdn n a b in 
+             (xO g,p)
+       | a, xO b => 
+             let (g,p) := Pggcdn n a b in 
+             let (aa,bb) := p in 
+             (g,(aa, xO bb))
+       | xO a, b => 
+             let (g,p) := Pggcdn n a b in 
+             let (aa,bb) := p in 
+             (g,(xO aa, bb))
+       | xI a', xI b' => match Pcompare a' b' Eq with 
+           | Eq => (a,(1,1))
+           | Lt => 
+                let (g,p) := Pggcdn n (b'-a') a in 
+                let (ba,aa) := p in 
+                (g,(aa, aa + xO ba))
+           | Gt => 
+                let (g,p) := Pggcdn n (a'-b') b in 
+                let (ab,bb) := p in 
+                (g,(bb+xO ab, bb))
+         end
+     end
+  end.
+
+Definition Pgcd (a b: positive) := Pgcdn (Psize a + Psize b)%nat a b.
+Definition Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b.
+
+Open Scope Z_scope.
+
+Definition Zgcd (a b : Z) : Z := match a,b with 
+  | Z0, _ => Zabs b 
+  | _, Z0 => Zabs a
+  | Zpos a, Zpos b => Zpos (Pgcd a b)
+  | Zpos a, Zneg b => Zpos (Pgcd a b)
+  | Zneg a, Zpos b => Zpos (Pgcd a b)
+  | Zneg a, Zneg b => Zpos (Pgcd a b)
+end.
+
+Definition Zggcd (a b : Z) : Z*(Z*Z) := match a,b with 
+  | Z0, _ => (Zabs b,(0, Zsgn b)) 
+  | _, Z0 => (Zabs a,(Zsgn a, 0))
+  | Zpos a, Zpos b => 
+     let (g,p) := Pggcd a b in 
+     let (aa,bb) := p in 
+     (Zpos g, (Zpos aa, Zpos bb))
+  | Zpos a, Zneg b => 
+     let (g,p) := Pggcd a b in 
+     let (aa,bb) := p in 
+     (Zpos g, (Zpos aa, Zneg bb))
+  | Zneg a, Zpos b => 
+     let (g,p) := Pggcd a b in 
+     let (aa,bb) := p in 
+     (Zpos g, (Zneg aa, Zpos bb))
+  | Zneg a, Zneg b =>
+     let (g,p) := Pggcd a b in 
+     let (aa,bb) := p in 
+     (Zpos g, (Zneg aa, Zneg bb))
+end.
+
+Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b.
+Proof.
+unfold Zgcd; destruct a; destruct b; auto with zarith.
+Qed.
+
+Lemma Psize_monotone : forall p q, Pcompare p q Eq = Lt -> (Psize p <= Psize q)%nat.
+Proof.
+induction p; destruct q; simpl; auto with arith; intros; try discriminate.
+intros; generalize (Pcompare_Gt_Lt _ _ H); auto with arith.
+intros; destruct (Pcompare_Lt_Lt _ _ H); auto with arith; subst; auto.
+Qed.
+
+Lemma Pminus_Zminus : forall a b, Pcompare a b Eq = Lt -> 
+ Zpos (b-a) = Zpos b - Zpos a.
+Proof.
+intros.
+repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
+rewrite nat_of_P_minus_morphism.
+apply inj_minus1.
+apply lt_le_weak.
+apply nat_of_P_lt_Lt_compare_morphism; auto.
+rewrite ZC4; rewrite H; auto.
+Qed.
+
+Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> 
+ Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. 
+Proof.
+intros.
+destruct H.
+constructor; auto.
+destruct H as (e,H2); exists (2*e); auto with zarith.
+rewrite Zpos_xO; rewrite H2; ring.
+intros.
+apply H1; auto.
+rewrite Zpos_xO in H2.
+rewrite Zpos_xI in H3.
+apply Gauss with 2; auto.
+apply bezout_rel_prime.
+destruct H3 as (bb, H3).
+apply Bezout_intro with bb (-Zpos b).
+omega.
+Qed.
+
+Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> 
+ Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcdn n a b)).
+Proof.
+intro n; pattern n; apply lt_wf_ind; clear n; intros.
+destruct n.
+simpl.
+destruct a; simpl in *; try inversion H0.
+destruct a.
+destruct b; simpl.
+case_eq (Pcompare a b Eq); intros.
+(* a = xI, b = xI, compare = Eq *)
+rewrite (Pcompare_Eq_eq _ _ H1); apply Zis_gcd_refl.
+(* a = xI, b = xI, compare = Lt *)
+apply Zis_gcd_sym.
+apply Zis_gcd_for_euclid with 1.
+apply Zis_gcd_sym.
+replace (Zpos (xI b) - 1 * Zpos (xI a)) with (Zpos(xO (b - a))).
+apply Zis_gcd_even_odd.
+apply H; auto.
+simpl in *.
+assert (Psize (b-a) <= Psize b)%nat.
+ apply Psize_monotone.
+ change (Zpos (b-a) < Zpos b).
+ rewrite (Pminus_Zminus _ _ H1).
+ assert (0 < Zpos a) by (compute; auto).
+ omega.
+omega.  
+rewrite Zpos_xO; do 2 rewrite Zpos_xI.
+rewrite Pminus_Zminus; auto.
+omega.
+(* a = xI, b = xI, compare = Gt *)
+apply Zis_gcd_for_euclid with 1.
+replace (Zpos (xI a) - 1 * Zpos (xI b)) with (Zpos(xO (a - b))).
+apply Zis_gcd_sym.
+apply Zis_gcd_even_odd.
+apply H; auto.
+simpl in *.
+assert (Psize (a-b) <= Psize a)%nat.
+ apply Psize_monotone.
+ change (Zpos (a-b) < Zpos a).
+ rewrite (Pminus_Zminus b a).
+ assert (0 < Zpos b) by (compute; auto).
+ omega.
+ rewrite ZC4; rewrite H1; auto.
+omega.  
+rewrite Zpos_xO; do 2 rewrite Zpos_xI.
+rewrite Pminus_Zminus; auto.
+omega.
+rewrite ZC4; rewrite H1; auto.
+(* a = xI, b = xO *)
+apply Zis_gcd_sym.
+apply Zis_gcd_even_odd.
+apply Zis_gcd_sym.
+apply H; auto.
+simpl in *; omega.
+(* a = xI, b = xH *)
+apply Zis_gcd_1.
+destruct b; simpl.
+(* a = xO, b = xI *)
+apply Zis_gcd_even_odd.
+apply H; auto.
+simpl in *; omega.
+(* a = xO, b = xO *)
+rewrite (Zpos_xO a); rewrite (Zpos_xO b); rewrite (Zpos_xO (Pgcdn n a b)).
+apply Zis_gcd_mult.
+apply H; auto.
+simpl in *; omega.
+(* a = xO, b = xH *)
+apply Zis_gcd_1.
+(* a = xH *)
+simpl; apply Zis_gcd_sym; apply Zis_gcd_1.
+Qed.
+
+Lemma Pgcd_correct : forall a b, Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcd a b)).
+Proof.
+unfold Pgcd; intros.
+apply Pgcdn_correct; auto.
+Qed.
+
+Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a b).
+Proof.
+destruct a.
+intros.
+simpl.
+apply Zis_gcd_0_abs.
+destruct b; simpl.
+apply Zis_gcd_0.
+apply Pgcd_correct.
+apply Zis_gcd_sym.
+apply Zis_gcd_minus; simpl.
+apply Pgcd_correct.
+destruct b; simpl.
+apply Zis_gcd_minus; simpl.
+apply Zis_gcd_sym.
+apply Zis_gcd_0.
+apply Zis_gcd_minus; simpl.
+apply Zis_gcd_sym.
+apply Pgcd_correct.
+apply Zis_gcd_sym.
+apply Zis_gcd_minus; simpl.
+apply Zis_gcd_minus; simpl.
+apply Zis_gcd_sym.
+apply Pgcd_correct.
+Qed.
+
+
+Lemma Pggcdn_gcdn : forall n a b, 
+ fst (Pggcdn n a b) = Pgcdn n a b.
+Proof.
+induction n.
+simpl; auto.
+destruct a; destruct b; simpl; auto.
+destruct (Pcompare a b Eq); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n (b-a) (xI a)) as (g,(aa,bb)); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n (a-b) (xI b)) as (g,(aa,bb)); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n (xI a) b) as (g,(aa,bb)); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n a (xI b)) as (g,(aa,bb)); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n a b) as (g,(aa,bb)); simpl; auto.
+Qed.
+
+Lemma Pggcd_gcd : forall a b, fst (Pggcd a b) = Pgcd a b.
+Proof.
+intros; exact (Pggcdn_gcdn (Psize a+Psize b)%nat a b).
+Qed.
+
+Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b.
+Proof.
+destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; 
+destruct (Pggcd p p0) as (g,(aa,bb)); simpl; auto.
+Qed.
+
+Open Scope positive_scope.
+
+Lemma Pggcdn_correct_divisors : forall n a b, 
+  let (g,p) := Pggcdn n a b in 
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
+Proof.
+induction n.
+simpl; auto.
+destruct a; destruct b; simpl; auto.
+case_eq (Pcompare a b Eq); intros.
+(* Eq *)
+rewrite Pmult_comm; simpl; auto.
+rewrite (Pcompare_Eq_eq _ _ H); auto.
+(* Lt *)
+generalize (IHn (b-a) (xI a)); destruct (Pggcdn n (b-a) (xI a)) as (g,(ba,aa)); simpl.
+intros (H0,H1); split; auto.
+rewrite Pmult_plus_distr_l.
+rewrite Pmult_xO_permute_r.
+rewrite <- H1; rewrite <- H0.
+simpl; f_equal; symmetry.
+apply Pplus_minus; auto.
+rewrite ZC4; rewrite H; auto.
+(* Gt *)
+generalize (IHn (a-b) (xI b)); destruct (Pggcdn n (a-b) (xI b)) as (g,(ab,bb)); simpl.
+intros (H0,H1); split; auto.
+rewrite Pmult_plus_distr_l.
+rewrite Pmult_xO_permute_r.
+rewrite <- H1; rewrite <- H0.
+simpl; f_equal; symmetry.
+apply Pplus_minus; auto.
+(* Then... *) 
+generalize (IHn (xI a) b); destruct (Pggcdn n (xI a) b) as (g,(ab,bb)); simpl.
+intros (H0,H1); split; auto.
+rewrite Pmult_xO_permute_r; rewrite H1; auto.
+generalize (IHn a (xI b)); destruct (Pggcdn n a (xI b)) as (g,(ab,bb)); simpl.
+intros (H0,H1); split; auto.
+rewrite Pmult_xO_permute_r; rewrite H0; auto.
+generalize (IHn a b); destruct (Pggcdn n a b) as (g,(ab,bb)); simpl.
+intros (H0,H1); split; subst; auto.
+Qed.
+
+Lemma Pggcd_correct_divisors : forall a b, 
+  let (g,p) := Pggcd a b in 
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
+Proof.
+intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b).
+Qed.
+
+Open Scope Z_scope.
+
+Lemma Zggcd_correct_divisors : forall a b, 
+  let (g,p) := Zggcd a b in 
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
+Proof.
+destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; 
+generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); 
+destruct 1; subst; auto.
+Qed.
+
+(** A version of [Zgcd] that doesn't use an explicit measure can be found 
+  in users's contribution [Orsay/QArith]. It is slightly more efficient after 
+  extraction, but cannot be used to compute within Coq. *)
+