ajout de QArith dans les theories standards

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

8 files changed, 1229 insertions, 7 deletions

diff --git a/.depend.coq b/.depend.coq
index d6babae10..caa85a2c6 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -280,6 +280,11 @@ theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relatio
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
 theories/Sorting/PermutSetoid.vo: theories/Sorting/PermutSetoid.v contrib/omega/Omega.vo theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Lists/SetoidList.vo
 theories/Sorting/PermutEq.vo: theories/Sorting/PermutEq.v contrib/omega/Omega.vo theories/Relations/Relations.vo theories/Setoids/Setoid.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo
+theories/QArith/QArith_base.vo: theories/QArith/QArith_base.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo theories/Setoids/Setoid.vo
+theories/QArith/Qreduction.vo: theories/QArith/Qreduction.v theories/QArith/QArith_base.vo theories/ZArith/Znumtheory.vo
+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
 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
@@ -295,9 +300,9 @@ contrib/ring/Quote.vo: contrib/ring/Quote.v
 contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo
 contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo
 contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo
-contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v
-contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo
-contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
+contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v theories/Lists/List.vo
+contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Lists/List.vo theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo
+contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v theories/Lists/List.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
 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
diff --git a/Makefile b/Makefile
index fe8d72908..526fdf1e5 100644
--- a/Makefile
+++ b/Makefile
@@ -869,6 +869,11 @@ ZARITHVO=\
  theories/ZArith/Zbool.vo	theories/ZArith/Zbinary.vo \
  theories/ZArith/Znumtheory.vo
 
+QARITHVO=\
+ theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \
+ theories/QArith/Qring.vo       theories/QArith/Qreals.vo \
+ theories/QArith/QArith.vo
+
 LISTSVO=\
  theories/Lists/MonoList.vo \
  theories/Lists/ListSet.vo   	theories/Lists/Streams.vo \
@@ -989,7 +994,7 @@ SETOIDSVO=theories/Setoids/Setoid.vo
 THEORIESVO =\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
   $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(INTMAPVO) \
-  $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) 
+  $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO)
 
 THEORIESLIGHTVO = $(INITVO) $(LOGICVO) $(ARITHVO)
 
@@ -1001,6 +1006,7 @@ arith: $(ARITHVO)
 bool: $(BOOLVO)
 narith: $(NARITHVO)
 zarith: $(ZARITHVO)
+qarith: $(QARITHVO)
 lists: $(LISTSVO)
 strings: $(STRINGSVO)
 sets: $(SETSVO)
@@ -1015,8 +1021,8 @@ allreals: $(ALLREALS)
 setoids: $(SETOIDSVO)
 sorting: $(SORTINGVO)
 
-noreal: logic arith bool zarith lists sets fsets intmap relations wellfounded \
-	setoids sorting
+noreal: logic arith bool zarith qarith lists sets fsets intmap relations \
+	wellfounded setoids sorting
 
 ###########################################################################
 # contribs (interface not included)
diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v
new file mode 100644
index 000000000..f7a28598e
--- /dev/null
+++ b/theories/QArith/QArith.v
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  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 Export QArith_base.
+Require Export Qring.
+Require Export Qreduction.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
new file mode 100644
index 000000000..3b01b83d9
--- /dev/null
+++ b/theories/QArith/QArith_base.v
@@ -0,0 +1,621 @@
+(************************************************************************)
+(*  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 Export ZArith.
+Require Export ZArithRing.
+Require Export Setoid.
+
+(** * Definition of [Q] and basic properties *)
+
+(** Rationals are pairs of [Z] and [positive] numbers. *)
+
+Record Q : Set := Qmake {Qnum : Z; Qden : positive}.
+
+Delimit Scope Q_scope with Q.
+Bind Scope Q_scope with Q.
+Arguments Scope Qmake [Z_scope positive_scope].
+Open Scope Q_scope.
+Ltac simpl_mult := repeat rewrite Zpos_mult_morphism.
+
+(** [a#b] denotes the fraction [a] over [b]. *)
+
+Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
+
+Definition inject_Z (x : Z) := Qmake x 1. 
+Arguments Scope inject_Z [Z_scope].
+
+Notation " 'QDen'  p " := (Zpos (Qden p)) (at level 20, no associativity) : Q_scope.
+Notation " 0 " := (0#1) : Q_scope.
+Notation " 1 " := (1#1) : Q_scope.
+
+Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.
+Definition Qle (x y : Q) := (Qnum x * QDen y <= Qnum y * QDen x)%Z.
+Definition Qlt (x y : Q) := (Qnum x * QDen y < Qnum y * QDen x)%Z.
+Notation Qgt := (fun x y : Q => Qlt y x).
+Notation Qge := (fun x y : Q => Qle y x).
+
+Infix "==" := Qeq (at level 70, no associativity) : Q_scope. 
+Infix "<" := Qlt : Q_scope.
+Infix "<=" := Qle : Q_scope.
+Infix ">" := Qgt : Q_scope. 
+Infix ">=" := Qge : Q_scope. 
+Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
+
+Hint Unfold Qeq Qle Qlt: qarith.
+Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
+
+(** Properties of equality. *)
+
+Theorem Qeq_refl : forall x, x == x.
+Proof.
+ auto with qarith.
+Qed.
+
+Theorem Qeq_sym : forall x y, x == y -> y == x. 
+Proof.
+ auto with qarith.
+Qed.
+
+Theorem Qeq_trans : forall x y z, x == y -> y == z -> x == z.
+Proof.
+unfold Qeq in |- *; intros.
+apply Zmult_reg_l with (QDen y). 
+auto with qarith.
+ring; rewrite H; ring.
+rewrite Zmult_assoc; rewrite H0; ring.
+Qed.
+
+(** Furthermore, this equality is decidable: *)
+
+Theorem Qeq_dec : forall x y, {x==y} + {~ x==y}.
+Proof.
+ intros; case (Z_eq_dec (Qnum x * QDen y) (Qnum y * QDen x)); auto.
+Defined.
+
+(** We now consider [Q] seen as a setoid. *)
+
+Definition Q_Setoid : Setoid_Theory Q Qeq.
+Proof.
+ split; unfold Qeq in |- *; auto; apply Qeq_trans.
+Qed.
+
+Add Setoid Q Qeq Q_Setoid as Qsetoid.
+
+Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith.
+Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith.
+Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith.
+
+(** The addition, multiplication and opposite are defined 
+   in the straightforward way: *)
+
+Definition Qplus (x y : Q) :=
+  (Qnum x * QDen y + Qnum y * QDen x) # (Qden x * Qden y).
+
+Definition Qmult (x y : Q) := (Qnum x * Qnum y) # (Qden x * Qden y). 
+
+Definition Qopp (x : Q) := (- Qnum x) # (Qden x).
+
+Definition Qminus (x y : Q) := Qplus x (Qopp y).
+
+Definition Qinv (x : Q) :=
+  match Qnum x with
+  | Z0 => 0
+  | Zpos p => (QDen x)#p
+  | Zneg p => (Zneg (Qden x))#p
+  end.
+
+Definition Qdiv (x y : Q) := Qmult x (Qinv y).
+
+Infix "+" := Qplus : Q_scope.
+Notation "- x" := (Qopp x) : Q_scope.
+Infix "-" := Qminus : Q_scope.
+Infix "*" := Qmult : Q_scope.
+Notation "/ x" := (Qinv x) : Q_scope. 
+Infix "/" := Qdiv : Q_scope. 
+
+(** A light notation for [Zpos] *)
+
+Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope.
+
+(** Setoid compatibility results *)
+
+Add Morphism Qplus : Qplus_comp. 
+Proof.
+unfold Qeq, Qplus; simpl.
+Open Scope Z_scope.
+intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
+simpl_mult; ring.
+replace (p1 * ('s2 * 'q2)) with (p1 * 'q2 * 's2) by ring.
+rewrite H.
+replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring.
+rewrite H0.
+ring.
+Open Scope Q_scope.
+Qed.
+
+Add Morphism Qopp : Qopp_comp.
+Proof.
+unfold Qeq, Qopp; simpl.
+intros; ring; rewrite H; ring.
+Qed.
+
+Add Morphism Qminus : Qminus_comp.
+Proof.
+intros.
+unfold Qminus. 
+rewrite H; rewrite H0; auto with qarith.
+Qed.
+
+Add Morphism Qmult : Qmult_comp.
+Proof.
+unfold Qeq; simpl.
+Open Scope Z_scope.
+intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
+intros; simpl_mult; ring.
+replace ('p2 * (q1 * s1)) with (q1 * 'p2 * s1) by ring.
+rewrite <- H.
+replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring.
+rewrite H0.
+ring.
+Open Scope Q_scope.
+Qed.
+
+Add Morphism Qinv : Qinv_comp.
+Proof.
+unfold Qeq, Qinv; simpl.
+Open Scope Z_scope.
+intros (p1, p2) (q1, q2); simpl.
+case p1; simpl.
+intros. 
+assert (q1 = 0).
+ elim (Zmult_integral q1 ('p2)); auto with zarith.
+ intros; discriminate.
+subst; auto. 
+case q1; simpl; intros; try discriminate.
+rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto.
+case q1; simpl; intros; try discriminate.
+rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto.
+Open Scope Q_scope.
+Qed.
+
+Add Morphism Qdiv : Qdiv_comp.
+Proof.
+intros; unfold Qdiv.
+rewrite H; rewrite H0; auto with qarith.
+Qed.
+
+Add Morphism Qle with signature Qeq ==> Qeq ==> iff as Qle_comp.
+Proof.
+cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<=x3 -> x2<=x4).
+split; apply H; assumption || (apply Qeq_sym ; assumption).
+
+unfold Qeq, Qle; simpl.
+Open Scope Z_scope.
+intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *.
+apply Zmult_le_reg_r with ('p2).
+unfold Zgt; auto.
+replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring.
+rewrite <- H.
+apply Zmult_le_reg_r with ('r2).
+unfold Zgt; auto.
+replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring.
+rewrite <- H0.
+replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring.
+replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring.
+auto with zarith.
+Open Scope Q_scope.
+Qed.
+
+Add Morphism Qlt with signature Qeq ==> Qeq ==> iff as  Qlt_comp.
+Proof.
+cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<x3 -> x2<x4).
+split; apply H; assumption || (apply Qeq_sym ; assumption).
+
+unfold Qeq, Qlt; simpl.
+Open Scope Z_scope.
+intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *.
+apply Zgt_lt.
+generalize (Zlt_gt _ _ H1); clear H1; intro H1.
+apply Zmult_gt_reg_r with ('p2); auto with zarith.
+replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring.
+rewrite <- H.
+apply Zmult_gt_reg_r with ('r2); auto with zarith.
+replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring.
+rewrite <- H0.
+replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring.
+replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. 
+apply Zlt_gt.
+apply Zmult_gt_0_lt_compat_l; auto with zarith.
+Open Scope Q_scope.
+Qed.
+
+(** [0] and [1] are apart *)
+
+Lemma Q_apart_0_1 : ~ 1 == 0.
+Proof.
+ unfold Qeq; auto with qarith.
+Qed.
+
+(** Addition is associative: *)
+
+Theorem Qplus_assoc : forall x y z, x+(y+z)==(x+y)+z.
+Proof.
+ intros (x1, x2) (y1, y2) (z1, z2).
+ unfold Qeq, Qplus; simpl; simpl_mult; ring.
+Qed.
+
+(** [0] is a neutral element for addition: *)
+
+Lemma Qplus_0_l : forall x, 0+x == x.
+Proof.
+ intros (x1, x2); unfold Qeq, Qplus; simpl; ring.
+Qed.
+
+Lemma Qplus_0_r : forall x, x+0 == x.
+Proof.
+ intros (x1, x2); unfold Qeq, Qplus; simpl.
+ rewrite Pmult_comm; simpl; ring.
+Qed. 
+
+(** Commutativity of addition: *)
+
+Theorem Qplus_comm : forall x y, x+y == y+x.
+Proof.
+ intros (x1, x2); unfold Qeq, Qplus; simpl.
+ intros; rewrite Pmult_comm; ring.
+Qed.
+
+(** Properties of [Qopp] *)
+
+Lemma Qopp_involutive : forall q, - -q == q.
+Proof.
+ red; simpl; intros; ring.
+Qed.
+
+Theorem Qplus_opp_r : forall q, q+(-q) == 0.
+Proof.
+ red; simpl; intro; ring.
+Qed.
+
+(** Multiplication is associative: *)
+
+Theorem Qmult_assoc : forall n m p, n*(m*p)==(n*m)*p.
+Proof.
+ intros; red; simpl; rewrite Pmult_assoc; ring.
+Qed.
+
+(** [1] is a neutral element for multiplication: *)
+
+Lemma Qmult_1_l : forall n, 1*n == n.
+Proof.
+ intro; red; simpl; destruct (Qnum n); auto.
+Qed.
+
+Theorem Qmult_1_r : forall n, n*1==n.
+Proof.
+ intro; red; simpl.
+ rewrite Zmult_1_r with (n := Qnum n).
+ rewrite Pmult_comm; simpl; trivial. 
+Qed.
+
+(** Commutativity of multiplication *)
+
+Theorem Qmult_comm : forall x y, x*y==y*x.
+Proof.
+ intros; red; simpl; rewrite Pmult_comm; ring.
+Qed.
+
+(** Distributivity *)
+
+Theorem Qmult_plus_distr_r : forall x y z, x*(y+z)==(x*y)+(x*z).
+Proof.
+intros (x1, x2) (y1, y2) (z1, z2).
+unfold Qeq, Qmult, Qplus; simpl; simpl_mult; ring.
+Qed.
+
+Theorem Qmult_plus_distr_l : forall x y z, (x+y)*z==(x*z)+(y*z).
+Proof.
+intros (x1, x2) (y1, y2) (z1, z2).
+unfold Qeq, Qmult, Qplus; simpl; simpl_mult; ring.
+Qed.
+
+(** Integrality *)
+
+Theorem Qmult_integral : forall x y, x*y==0 -> x==0 \/ y==0.
+Proof.
+ intros (x1,x2) (y1,y2).
+ unfold Qeq, Qmult; simpl; intros.
+ destruct (Zmult_integral (x1*1)%Z (y1*1)%Z); auto.
+ rewrite <- H; ring.
+Qed.
+
+Theorem Qmult_integral_l : forall x y, ~ x == 0 -> x*y == 0 -> y == 0.
+Proof.
+ intros (x1, x2) (y1, y2).
+ unfold Qeq, Qmult; simpl; intros.
+ apply Zmult_integral_l with x1; auto with zarith.
+ rewrite <- H0; ring.
+Qed.
+
+(** Inverse and division. *) 
+
+Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1.
+Proof.
+ intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl;
+  intros; simpl_mult; try ring.
+ elim H; auto. 
+Qed.
+
+Lemma Qinv_mult_distr : forall p q, / (p * q) == /p * /q.
+Proof.
+intros (x1,x2) (y1,y2); unfold Qeq, Qinv, Qmult; simpl.
+destruct x1; simpl; auto; 
+ destruct y1; simpl; auto.
+Qed.
+
+Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x.
+Proof.
+ intros; unfold Qdiv.
+ rewrite <- (Qmult_assoc x y (Qinv y)).
+ rewrite (Qmult_inv_r y H).
+ apply Qmult_1_r.
+Qed.
+
+Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x.
+Proof.
+ intros; unfold Qdiv.
+ rewrite (Qmult_assoc y x (Qinv y)).
+ rewrite (Qmult_comm y x).
+ fold (Qdiv (Qmult x y) y).
+ apply Qdiv_mult_l; auto.
+Qed.
+
+(** Properties of order upon Q. *)
+
+Lemma Qle_refl : forall x, x<=x.
+Proof.
+unfold Qle; auto with zarith.
+Qed.
+
+Lemma Qle_antisym : forall x y, x<=y -> y<=x -> x==y.
+Proof.
+unfold Qle, Qeq; auto with zarith.
+Qed.
+
+Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z.
+Proof.
+unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
+Open Scope Z_scope.
+apply Zmult_le_reg_r with ('y2).
+red; trivial.
+apply Zle_trans with (y1 * 'x2 * 'z2).
+replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
+apply Zmult_le_compat_r; auto with zarith. 
+replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
+replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
+apply Zmult_le_compat_r; auto with zarith. 
+Open Scope Q_scope.
+Qed.
+
+Lemma Qlt_not_eq : forall x y, x<y -> ~ x==y.
+Proof.
+unfold Qlt, Qeq; auto with zarith.
+Qed.
+
+(** Large = strict or equal *)
+
+Lemma Qlt_le_weak : forall x y, x<y -> x<=y.
+Proof.
+unfold Qle, Qlt; auto with zarith.
+Qed.
+
+Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.
+Proof.
+unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
+Open Scope Z_scope.
+apply Zgt_lt.
+apply Zmult_gt_reg_r with ('y2).
+red; trivial.
+apply Zgt_le_trans with (y1 * 'x2 * 'z2).
+replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
+replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
+apply Zmult_gt_compat_r; auto with zarith. 
+replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
+apply Zmult_le_compat_r; auto with zarith. 
+Open Scope Q_scope.
+Qed.
+
+Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z.
+Proof.
+unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
+Open Scope Z_scope.
+apply Zgt_lt.
+apply Zmult_gt_reg_r with ('y2).
+red; trivial.
+apply Zle_gt_trans with (y1 * 'x2 * 'z2).
+replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
+replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
+apply Zmult_le_compat_r; auto with zarith. 
+replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
+apply Zmult_gt_compat_r; auto with zarith. 
+Open Scope Q_scope.
+Qed.
+
+Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z.
+Proof.
+intros.
+apply Qle_lt_trans with y; auto.
+apply Qlt_le_weak; auto.
+Qed.
+
+(** [x<y] iff [~(y<=x)] *)
+
+Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x.
+Proof.
+unfold Qle, Qlt; auto with zarith.
+Qed.
+
+Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x.
+Proof.
+unfold Qle, Qlt; auto with zarith.
+Qed.
+
+Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x.
+Proof.
+unfold Qle, Qlt; auto with zarith.
+Qed.
+
+Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x.
+Proof.
+unfold Qle, Qlt; auto with zarith.
+Qed.
+
+Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.
+Proof.
+unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto.
+Qed.
+
+(** Some decidability results about orders. *)
+
+Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}.
+Proof.
+unfold Qlt, Qle, Qeq; intros.
+exact (Z_dec' (Qnum x * QDen y) (Qnum y * QDen x)).
+Defined.
+
+Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}.
+Proof.
+unfold Qlt, Qle; intros.
+exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)).
+Defined.
+
+(** Compatibility of operations with respect to order. *)
+
+Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p.
+Proof.
+intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.
+do 2 rewrite <- Zopp_mult_distr_l; omega.
+Qed.
+
+Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
+Proof.
+intros (x1,x2) (y1,y2); unfold Qle; simpl.
+rewrite <- Zopp_mult_distr_l.
+split; omega.
+Qed.
+
+Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p.
+Proof.
+intros (x1,x2) (y1,y2); unfold Qlt; simpl.
+rewrite <- Zopp_mult_distr_l.
+split; omega.
+Qed.
+
+Lemma Qplus_le_compat :
+ forall x y z t, x<=y -> z<=t -> x+z <= y+t.
+Proof.
+unfold Qplus, Qle; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2);
+ simpl; simpl_mult.
+Open Scope Z_scope.
+intros.
+match goal with |- ?a <= ?b => ring a; ring b end.
+apply Zplus_le_compat.
+replace ('t2 * ('y2 * (z1 * 'x2))) with (z1 * 't2 * ('y2 * 'x2)) by ring.
+replace ('z2 * ('x2 * (t1 * 'y2))) with (t1 * 'z2 * ('y2 * 'x2)) by ring.
+apply Zmult_le_compat_r; auto with zarith.
+replace ('t2 * ('y2 * ('z2 * x1))) with (x1 * 'y2 * ('z2 * 't2)) by ring.
+replace ('z2 * ('x2 * ('t2 * y1))) with (y1 * 'x2 * ('z2 * 't2)) by ring.
+apply Zmult_le_compat_r; auto with zarith.
+Open Scope Q_scope.
+Qed.
+
+Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.
+Proof.
+intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
+Open Scope Z_scope.
+intros; simpl_mult.
+replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
+replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
+apply Zmult_le_compat_r; auto with zarith.
+Open Scope Q_scope.
+Qed.
+
+Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 <  z  -> x*z <= y*z -> x <= y.
+Proof.
+intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
+Open Scope Z_scope.
+simpl_mult.
+replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
+replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
+intros; apply Zmult_le_reg_r with (c1*'c2); auto with zarith.
+Open Scope Q_scope.
+Qed.
+
+Lemma Qmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.
+Proof.
+intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
+Open Scope Z_scope.
+intros; simpl_mult.
+replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
+replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
+apply Zmult_lt_compat_r; auto with zarith.
+apply Zmult_lt_0_compat.
+omega.
+compute; auto.
+Open Scope Q_scope.
+Qed.
+
+(** Rational to the n-th power *)
+
+Fixpoint Qpower (q:Q)(n:nat) { struct n } : Q := 
+ match n with 
+  | O => 1
+  | S n => q * (Qpower q n)
+ end. 
+
+Notation " q ^ n " := (Qpower q n) : Q_scope.
+
+Lemma Qpower_1 : forall n, 1^n == 1.
+Proof.
+induction n; simpl; auto with qarith.
+rewrite IHn; auto with qarith.
+Qed.
+
+Lemma Qpower_0 : forall n, n<>O -> 0^n == 0.
+Proof.
+destruct n; simpl.
+destruct 1; auto.
+intros. 
+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 Qle_trans with (0*(p^n)).
+compute; intro; discriminate.
+apply Qmult_le_compat_r; auto.
+Qed.
+
+Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n.
+Proof.
+induction n.
+compute; auto.
+simpl.
+intros; rewrite IHn; clear IHn.
+unfold Qdiv; rewrite Qinv_mult_distr.
+setoid_replace (1#p) with (/ inject_Z ('p)).
+apply Qeq_refl.
+compute; auto.
+Qed.
+
+
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
new file mode 100644
index 000000000..e4b22dd56
--- /dev/null
+++ b/theories/QArith/Qreals.v
@@ -0,0 +1,213 @@
+(************************************************************************)
+(*  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 Export Rbase.
+Require Export QArith_base.
+
+(** * A field tactic for rational numbers. *)
+
+(** Since field cannot operate on setoid datatypes (yet?), 
+  we translate Q goals into reals before applying field. *)
+
+Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R.
+intros; apply not_O_IZR; auto with qarith.
+Qed.
+
+Hint Immediate IZR_nz.
+Hint Resolve Rmult_integral_contrapositive.
+
+Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.
+
+Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y.
+Proof.
+unfold Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
+ intros.
+apply eq_IZR.
+do 2 rewrite mult_IZR.
+set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
+ set (X2 := IZR (Zpos x2)) in *.
+set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
+ set (Y2 := IZR (Zpos y2)) in *.
+assert ((X2 * X1 * / X2)%R = (X2 * (Y1 * / Y2))%R).
+rewrite <- H; field; auto.
+rewrite Rinv_r_simpl_m in H0; auto; rewrite H0; field; auto.
+Qed.
+
+Lemma Qeq_eqR : forall x y : Q, x==y -> Q2R x = Q2R y.
+Proof.
+unfold Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
+ intros.
+set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
+ set (X2 := IZR (Zpos x2)) in *.
+set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
+ set (Y2 := IZR (Zpos y2)) in *.
+assert ((X1 * Y2)%R = (Y1 * X2)%R).
+ unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR.
+ apply IZR_eq; auto.
+clear H.
+field; auto.
+rewrite <- H0; field; auto.
+Qed.
+
+Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.
+Proof.
+unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
+ intros.
+apply le_IZR.
+do 2 rewrite mult_IZR.
+set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
+ set (X2 := IZR (Zpos x2)) in *.
+set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
+ set (Y2 := IZR (Zpos y2)) in *.
+replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto).
+replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto).
+apply Rmult_le_compat_r; auto.
+apply Rmult_le_pos.
+unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le;
+ auto with zarith.
+unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le;
+ auto with zarith.
+Qed.
+
+Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R.
+Proof.
+unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
+ intros.
+set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
+ set (X2 := IZR (Zpos x2)) in *.
+set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
+ set (Y2 := IZR (Zpos y2)) in *.
+assert (X1 * Y2 <= Y1 * X2)%R.
+ unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR.
+ apply IZR_le; auto.
+clear H.
+replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto).
+replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto).
+apply Rmult_le_compat_r; auto.
+apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat.
+unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
+ auto with zarith.
+unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
+ auto with zarith.
+Qed.
+
+Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y.
+Proof.
+unfold Qlt, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
+ intros.
+apply lt_IZR.
+do 2 rewrite mult_IZR.
+set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
+ set (X2 := IZR (Zpos x2)) in *.
+set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
+ set (Y2 := IZR (Zpos y2)) in *.
+replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto).
+replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto).
+apply Rmult_lt_compat_r; auto.
+apply Rmult_lt_0_compat.
+unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
+ auto with zarith.
+unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
+ auto with zarith.
+Qed.
+
+Lemma Qlt_Rlt : forall x y : Q, x<y -> (Q2R x < Q2R y)%R.
+Proof.
+unfold Qlt, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
+ intros.
+set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
+ set (X2 := IZR (Zpos x2)) in *.
+set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
+ set (Y2 := IZR (Zpos y2)) in *.
+assert (X1 * Y2 < Y1 * X2)%R.
+ unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR.
+ apply IZR_lt; auto.
+clear H.
+replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto).
+replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto).
+apply Rmult_lt_compat_r; auto.
+apply Rmult_lt_0_compat; apply Rinv_0_lt_compat.
+unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
+ auto with zarith.
+unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
+ auto with zarith.
+Qed.
+
+Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R.
+Proof.
+unfold Qplus, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2);
+ unfold Qden, Qnum in |- *.
+simpl_mult.
+rewrite plus_IZR.
+do 3 rewrite mult_IZR.
+field; auto.
+Qed.
+
+Lemma Q2R_mult : forall x y : Q, Q2R (x*y) = (Q2R x * Q2R y)%R.
+Proof.
+unfold Qmult, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2);
+ unfold Qden, Qnum in |- *.
+simpl_mult.
+do 2 rewrite mult_IZR.
+field; auto.
+Qed.
+
+Lemma Q2R_opp : forall x : Q, Q2R (- x) = (- Q2R x)%R.
+Proof.
+unfold Qopp, Qeq, Q2R in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
+rewrite Ropp_Ropp_IZR.
+field; auto.
+Qed.
+
+Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R.
+unfold Qminus in |- *; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto.
+Qed.
+
+Lemma Q2R_inv : forall x : Q, ~ x==0#1 -> Q2R (/x) = (/ Q2R x)%R.
+Proof.
+unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
+case x1.
+simpl in |- *; intros; elim H; trivial.
+intros; field; auto.
+apply Rmult_integral_contrapositive; split; auto.
+apply Rmult_integral_contrapositive; split; auto.
+apply Rinv_neq_0_compat; auto.
+intros; field; auto.
+do 2 rewrite <- mult_IZR.
+simpl in |- *; rewrite Pmult_comm; auto.
+apply Rmult_integral_contrapositive; split; auto.
+apply Rmult_integral_contrapositive; split; auto.
+apply not_O_IZR; auto with qarith.
+apply Rinv_neq_0_compat; auto.
+Qed.
+
+Lemma Q2R_div :
+ forall x y : Q, ~ y==0#1 -> Q2R (x/y) = (Q2R x / Q2R y)%R.
+Proof.
+unfold Qdiv, Rdiv in |- *.
+intros; rewrite Q2R_mult.
+rewrite Q2R_inv; auto.
+Qed.
+
+Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.
+
+Ltac QField := apply eqR_Qeq; autorewrite with q2r_simpl; try field; auto.
+
+(** Examples of use: *)
+
+Goal forall x y z : Q, (x+y)*z == (x*z)+(y*z).
+intros; QField.
+Abort.
+
+Goal forall x y : Q, ~ y==0#1 -> (x/y)*y == x.
+intros; QField.
+intro; apply H; apply eqR_Qeq.
+rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real.
+Abort.
\ No newline at end of file
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
new file mode 100644
index 000000000..b818f744f
--- /dev/null
+++ b/theories/QArith/Qreduction.v
@@ -0,0 +1,265 @@
+(************************************************************************)
+(*  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*)
+
+(** * Normalisation functions for rational numbers. *)
+
+Require Export QArith_base.
+Require Export Znumtheory.
+
+(** First, a function that (tries to) build a positive back from a Z. *)
+
+Definition Z2P (z : Z) :=
+  match z with
+  | Z0 => 1%positive
+  | Zpos p => p
+  | Zneg p => p
+  end.
+
+Lemma Z2P_correct : forall z : Z, (0 < z)%Z -> Zpos (Z2P z) = z.
+Proof.
+ simple destruct z; simpl in |- *; auto; intros; discriminate.
+Qed.
+
+Lemma Z2P_correct2 : forall z : Z, 0%Z <> z -> Zpos (Z2P z) = Zabs z.
+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).
+
+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.
+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.
+Open Scope Z_scope.
+intuition.
+rewrite <- H in H0,H1; clear H.
+rewrite H3; rewrite H4.
+assert (0 <> g).
+  intro; subst g; discriminate.
+
+assert (0 < dd).
+  apply Zmult_gt_0_lt_0_reg_r with g.
+  omega.
+  rewrite Zmult_comm.
+  rewrite <- H4; compute; auto.
+rewrite Z2P_correct; auto.
+ring.
+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 *.
+Open Scope Z_scope.
+generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) 
+ (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)).
+destruct (Zggcd a (Zpos b)) as (g,(aa,bb)).
+generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) 
+ (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)).
+destruct (Zggcd c (Zpos d)) as (g',(cc,dd)).
+simpl.
+intro H; rewrite <- H; clear H.
+intros Hg'1 Hg'2 (Hg'3,Hg'4).
+intro H; rewrite <- H; clear H.
+intros Hg1 Hg2 (Hg3,Hg4).
+intros.
+assert (g <> 0).
+  intro; subst g; discriminate.
+assert (g' <> 0).
+  intro; subst g'; discriminate.
+elim (rel_prime_cross_prod aa bb cc dd).
+congruence.
+unfold rel_prime in |- *.
+(*rel_prime*)
+constructor.
+exists aa; auto with zarith.
+exists bb; auto with zarith.
+intros.
+inversion Hg1.
+destruct (H6 (g*x)).
+rewrite Hg3.
+destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring.
+rewrite Hg4.
+destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring.
+exists q.
+apply Zmult_reg_l with g; auto.
+pattern g at 1; rewrite H7; ring.
+(* /rel_prime *)
+unfold rel_prime in |- *.
+(* rel_prime *)
+constructor.
+exists cc; auto with zarith.
+exists dd; auto with zarith.
+intros.
+inversion Hg'1.
+destruct (H6 (g'*x)).
+rewrite Hg'3.
+destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring.
+rewrite Hg'4.
+destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring.
+exists q.
+apply Zmult_reg_l with g'; auto.
+pattern g' at 1; rewrite H7; ring.
+(* /rel_prime *)
+assert (0<bb); [|auto with zarith].
+  apply Zmult_gt_0_lt_0_reg_r with g.
+  omega.
+  rewrite Zmult_comm.
+  rewrite <- Hg4; compute; auto.
+assert (0<dd); [|auto with zarith].
+  apply Zmult_gt_0_lt_0_reg_r with g'.
+  omega.
+  rewrite Zmult_comm.
+  rewrite <- Hg'4; compute; auto.
+apply Zmult_reg_l with (g'*g).
+intro H2; elim (Zmult_integral _ _ H2); auto.
+replace (g'*g*(aa*dd)) with ((g*aa)*(g'*dd)); [|ring].
+replace (g'*g*(bb*cc)) with ((g'*cc)*(g*bb)); [|ring].
+rewrite <- Hg3; rewrite <- Hg4; rewrite <- Hg'3; rewrite <- Hg'4; auto.
+Open Scope Q_scope.
+Qed.
+
+Add Morphism Qred : Qred_comp. 
+Proof.
+intros q q' H.
+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). 
+
+Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q).
+Proof.
+intros; unfold Qplus' in |- *; apply Qred_correct; auto.
+Qed.
+
+Lemma Qmult'_correct : forall p q : Q, (Qmult' p q)==(Qmult p q).
+Proof.
+intros; unfold Qmult' in |- *; apply Qred_correct; auto.
+Qed.
+
+Add Morphism Qplus' : Qplus'_comp.
+Proof.
+intros; unfold Qplus' in |- *.
+rewrite H; rewrite H0; auto with qarith.
+Qed.
+
+Add Morphism Qmult' : Qmult'_comp.
+intros; unfold Qmult' in |- *.
+rewrite H; rewrite H0; auto with qarith.
+Qed.
+
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
new file mode 100644
index 000000000..84a968475
--- /dev/null
+++ b/theories/QArith/Qring.v
@@ -0,0 +1,91 @@
+(************************************************************************)
+(*  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 Ring.
+Require Export Setoid_ring.
+Require Export QArith_base.
+
+(** * A ring tactic for rational numbers *)
+
+Definition Qeq_bool (x y : Q) :=
+  if Qeq_dec x y then true else false.
+
+Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y.
+intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
+intros _ H; inversion H.
+Qed.
+
+Definition Qsrt : Setoid_Ring_Theory Qeq Qplus Qmult 1 0 Qopp Qeq_bool.
+Proof.
+constructor.
+exact Qplus_comm.
+exact Qplus_assoc.
+exact Qmult_comm.
+exact Qmult_assoc.
+exact Qplus_0_l.
+exact Qmult_1_l.
+exact Qplus_opp_r.
+exact Qmult_plus_distr_l.
+unfold Is_true; intros x y; generalize (Qeq_bool_correct x y);
+ case (Qeq_bool x y); auto.
+Qed.
+
+Add Setoid Ring Q Qeq Q_Setoid Qplus Qmult 1 0 Qopp Qeq_bool
+ Qplus_comp Qmult_comp Qopp_comp Qsrt
+ [ Qmake (*inject_Z*)  Zpos 0%Z Zneg xI xO 1%positive ].
+
+(** Exemple of use: *)
+
+Section Examples. 
+
+Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
+intros.
+ring.
+Qed.
+
+Let ex2 : forall x y : Q, x+y == y+x.
+intros. 
+ring.
+Qed.
+
+Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
+intros.
+ring.
+Qed.
+
+Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
+ring.
+Qed.
+
+Let ex5 : 1+1 == 2#1.
+ring.
+Qed.
+
+Let ex6 : (1#1)+(1#1) == 2#1.
+ring.
+Qed.
+
+Let ex7 : forall x : Q, x-x== 0#1.
+intro.
+ring.
+Qed.
+
+End Examples.
+
+Lemma Qopp_plus : forall a b,  -(a+b) == -a + -b.
+Proof.
+intros; ring.
+Qed.
+
+Lemma Qopp_opp : forall q, - -q==q.
+Proof.
+intros; ring.
+Qed.
+
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 16e2ff325..9cf394468 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 (***********************************************************)
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 (***********************************************************)
 
 Require Export BinPos.
@@ -703,6 +703,12 @@ Qed.
 (**********************************************************************)
 (** Properties of multiplication on binary integer numbers *)
 
+Theorem Zpos_mult_morphism : 
+ forall p q:positive, Zpos (p*q) = Zpos p * Zpos q.
+Proof.
+auto.
+Qed.
+
 (** One is neutral for multiplication *)
 
 Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n.
@@ -935,6 +941,8 @@ Proof.
 intros; symmetry  in |- *; apply Zmult_succ_l.
 Qed.
 
+
+
 (** Misc redundant properties *)
 
 Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0.