In agreement with Laurent Thery, start migration of auxiliary results

present in Ints. For the moment, mainly: 
 - Q parts go in QArith
 - Some of the Zdivide & Zgcd stuff go in Znumtheory

More to come ...



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

16 files changed, 522 insertions, 523 deletions

diff --git a/theories/Ints/Q/QBAux.v b/theories/Ints/Q/QBAux.v
deleted file mode 100644
index 6b4bfc8140..0000000000
--- a/theories/Ints/Q/QBAux.v
+++ /dev/null
@@ -1,75 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
-
-(**********************************************************************
-     QBAux.v
-
-     Auxillary functions & Theorems for Q
- **********************************************************************)
-
-Require Import ZAux.
-Require Import QArith.
-Require Import Qcanon.
-
- Theorem Qred_opp: forall q, 
-   (Qred (-q) = - (Qred q))%Q.
- intros (x, y); unfold Qred; simpl.
- rewrite Zggcd_opp; case Zggcd; intros p1 (p2, p3); simpl.
- unfold Qopp; auto.
- Qed.
-
- Theorem Qcompare_red: forall x y,
-  Qcompare x y = Qcompare (Qred x) (Qred y).
- intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct.
- Qed.
-
-
-
- Theorem Qpower_decomp: forall p x y,
-  Qpower_positive (x #y) p == x ^ Zpos p # (Z2P ((Zpos y) ^ Zpos p)).
- Proof.
- intros p; elim p; clear p.
-   intros p Hrec x y.
-      unfold Qmult; simpl; rewrite Hrec.
-   rewrite xI_succ_xO; rewrite <- Pplus_diag; rewrite Pplus_one_succ_l.
-   repeat rewrite Zpower_pos_is_exp.
-   red; unfold Qmult, Qnum, Qden, Zpower.
-   repeat rewrite Zpos_mult_morphism.
-   repeat rewrite Z2P_correct.
-   2: apply ZAux.Zpower_pos_pos; red; auto.
-   2: repeat apply Zmult_lt_0_compat; auto;
-      apply ZAux.Zpower_pos_pos; red; auto.
-   repeat rewrite ZAux.Zpower_pos_1_r; ring.
-
-   intros p Hrec x y.
-      unfold Qmult; simpl; rewrite Hrec.
-   rewrite <- Pplus_diag.
-   repeat rewrite Zpower_pos_is_exp.
-   red; unfold Qmult, Qnum, Qden, Zpower.
-   repeat rewrite Zpos_mult_morphism.
-   repeat rewrite Z2P_correct; try ring.
-   apply ZAux.Zpower_pos_pos; red; auto.
-   repeat apply Zmult_lt_0_compat; auto;
-      apply ZAux.Zpower_pos_pos; red; auto.
- intros x y.
- unfold Qmult; simpl.
- red; simpl; rewrite ZAux.Zpower_pos_1_r; 
-   rewrite Zpos_mult_morphism; ring.
- Qed.
-
-
- Theorem Qc_decomp: forall (x y: Qc),
-    (Qred x = x -> Qred y = y -> (x:Q) = y)-> x = y.
-  intros (q, Hq) (q', Hq'); simpl; intros H.
-  assert (H1 := H Hq Hq').
-  subst q'.
-  assert (Hq = Hq'). 
-  apply Eqdep_dec.eq_proofs_unicity; auto; intros.
-  repeat decide equality.
-  congruence.
- Qed.
diff --git a/theories/Ints/Tactic.v b/theories/Ints/Tactic.v
index 08daffa551..6837f59220 100644
--- a/theories/Ints/Tactic.v
+++ b/theories/Ints/Tactic.v
@@ -52,14 +52,6 @@ Ltac  contradict name :=
 
 
 (**************************************
-  A tactic to do case analysis keeping the equality
-**************************************)
-
-Ltac case_eq name :=
-  generalize (refl_equal name); pattern name at -1 in |- *; case name.
-
-
-(**************************************
  A tactic to use f_equal? theorems 
 **************************************)
 
diff --git a/theories/Ints/Z/ZAux.v b/theories/Ints/Z/ZAux.v
index 83c54bd478..83337ee508 100644
--- a/theories/Ints/Z/ZAux.v
+++ b/theories/Ints/Z/ZAux.v
@@ -619,169 +619,50 @@ Qed.
 (**************************************
  Properties of Zdivide
 **************************************)
- 
-Theorem Zdivide_trans: forall a b c,  (a | b) -> (b | c) ->  (a | c).
-intros a b c [d H1] [e H2]; exists (d * e)%Z; auto with zarith.
-rewrite H2; rewrite H1; ring.
-Qed.
-
-Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) ->  (a | b).
-intros a b [x H]; subst b.
-pattern (Zabs a); apply Zabs_intro.
-exists (- x); ring.
-exists x; ring.
-Qed.
- 
-Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) ->  (Zabs a | b).
-intros a b [x H]; subst b.
-pattern (Zabs a); apply Zabs_intro.
-exists (- x);  ring.
-exists x; ring.
-Qed.
-
-Theorem Zdivide_le: forall a b, 0 <= a -> 0 < b -> (a | b) ->  a <= b.
-intros a b H1 H2 [q H3]; subst b.
-case (Zle_lt_or_eq 0 a); auto with zarith; intros H3.
-case (Zle_lt_or_eq 0 q); auto with zarith.
-apply (Zmult_le_0_reg_r a); auto with zarith.
-intros H4; apply Zle_trans with (1 * a); auto with zarith.
-intros H4; subst q; contradict H2; auto with zarith.
-Qed.
-
-Theorem Zdivide_Zdiv_eq: forall a b, 0 < a -> (a | b) ->  b = a * (b / a).
-intros a b Hb Hc.
-pattern b at 1; rewrite (Z_div_mod_eq b a); auto with zarith.
-rewrite (Zdivide_mod b a); auto with zarith.
-Qed.
- 
-Theorem Zdivide_Zdiv_lt_pos:
- forall a b, 1 < a -> 0 < b -> (a | b) ->  0 < b / a < b .
-intros a b H1 H2 H3; split.
-apply Zmult_lt_reg_r with a; auto with zarith.
-rewrite (Zmult_comm (Zdiv b a)); rewrite <- Zdivide_Zdiv_eq; auto with zarith.
-apply Zmult_lt_reg_r with a; auto with zarith.
-(repeat rewrite (fun x => Zmult_comm x a)); auto with zarith.
-rewrite <- Zdivide_Zdiv_eq; auto with zarith.
-pattern b at 1; replace b with (1 * b); auto with zarith.
-apply Zmult_lt_compat_r; auto with zarith.
-Qed.
 
-Theorem Zmod_divide_minus: forall a b c, 0 < b -> a mod b = c -> (b | a - c).
-intros a b c H H1; apply Zmod_divide; auto with zarith.
-rewrite Zmod_minus; auto.
-rewrite H1; pattern c at 1; rewrite <- (Zmod_def_small c b); auto with zarith.
-rewrite Zminus_diag; apply Zmod_def_small; auto with zarith.
-subst; apply Z_mod_lt; auto with zarith.
+Theorem Zmod_divide_minus: forall a b c : Z, 
+ 0 < b -> a mod b = c -> (b | a - c).
+Proof.
+  intros a b c H H1; apply Zmod_divide; auto with zarith.
+  rewrite Zmod_minus; auto.
+  rewrite H1; pattern c at 1; rewrite <- (Zmod_def_small c b); auto with zarith.
+  rewrite Zminus_diag; apply Zmod_def_small; auto with zarith.
+  subst; apply Z_mod_lt; auto with zarith.
 Qed.
 
-Theorem Zdivide_mod_minus: forall a b c, 0 <= c < b -> (b | a -c) -> (a mod b) = c.
-intros a b c (H1, H2) H3; assert (0 < b); try apply Zle_lt_trans with c; auto.
-replace a with ((a - c) + c); auto with zarith.
-rewrite Zmod_plus; auto with zarith.
-rewrite (Zdivide_mod (a -c) b); try rewrite Zplus_0_l; auto with zarith.
-rewrite Zmod_mod; try apply Zmod_def_small; auto with zarith.
+Theorem Zdivide_mod_minus: forall a b c : Z, 
+ 0 <= c < b -> (b | a -c) -> (a mod b) = c.
+Proof.
+  intros a b c (H1, H2) H3; assert (0 < b); try apply Zle_lt_trans with c; auto.
+  replace a with ((a - c) + c); auto with zarith.
+  rewrite Zmod_plus; auto with zarith.
+  rewrite (Zdivide_mod (a -c) b); try rewrite Zplus_0_l; auto with zarith.
+  rewrite Zmod_mod; try apply Zmod_def_small; auto with zarith.
 Qed.
 
 Theorem Zmod_closeby_eq: forall a b n,  0 <= a -> 0 <= b < n -> a - b < n -> a mod n = b -> a = b.
-intros a b n H H1 H2 H3.
-case (Zle_or_lt 0 (a - b)); intros H4.
-case Zle_lt_or_eq with (1 := H4); clear H4; intros H4; auto with zarith.
-contradict H2; apply Zle_not_lt; apply Zdivide_le; auto with zarith.
-apply Zmod_divide_minus; auto with zarith.
-rewrite <- (Zmod_def_small a n); try split; auto with zarith.
+Proof.
+  intros a b n H H1 H2 H3.
+  case (Zle_or_lt 0 (a - b)); intros H4.
+  case Zle_lt_or_eq with (1 := H4); clear H4; intros H4; auto with zarith.
+  absurd_hyp H2; auto.
+  apply Zle_not_lt; apply Zdivide_le; auto with zarith.
+  apply Zmod_divide_minus; auto with zarith.
+  rewrite <- (Zmod_def_small a n); try split; auto with zarith.
 Qed.
 
 Theorem Zpower_divide: forall p q, 0 < q -> (p | p ^ q).
-intros p q H; exists (p ^(q - 1)).
-pattern p at 3; rewrite <- (Zpower_exp_1 p); rewrite <- Zpower_exp; try eq_tac; auto with zarith.
+Proof.
+  intros p q H; exists (p ^(q - 1)).
+  pattern p at 3; rewrite <- (Zpower_exp_1 p); rewrite <- Zpower_exp; try eq_tac; auto with zarith.
 Qed.
 
+
 (**************************************
  Properties of Zis_gcd 
 **************************************)
- 
-Theorem Zis_gcd_unique:
- forall (a b c d : Z), Zis_gcd a b c -> Zis_gcd b a d ->  c = d \/ c = (- d).
-intros a b c d H1 H2.
-inversion_clear H1 as [Hc1 Hc2 Hc3].
-inversion_clear H2 as [Hd1 Hd2 Hd3].
-assert (H3: Zdivide c d); auto.
-assert (H4: Zdivide d c); auto.
-apply Zdivide_antisym; auto.
-Qed.
-
-
-Theorem Zis_gcd_gcd: forall a b c, 0 <= c ->  Zis_gcd a b c -> Zgcd a b = c.
-intros a b c H1 H2.
-case (Zis_gcd_uniqueness_apart_sign a b c (Zgcd a b)); auto.
-apply Zgcd_is_gcd; auto.
-case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; subst; auto.
-intros H3; subst; contradict H1.
-apply Zle_not_lt; generalize (Zgcd_is_pos a b); auto with zarith.
-case (Zgcd a b); simpl; auto; intros; discriminate.
-Qed.
-
-
-Theorem Zdivide_Zgcd: forall p q r, (p | q) -> (p | r) -> (p | Zgcd q r).
-intros p q r H1 H2.
-assert (H3: (Zis_gcd q r (Zgcd q r))).
-apply Zgcd_is_gcd.
-inversion_clear H3; auto.
-Qed.
-
- Theorem Zggcd_opp: 
-   forall x y, Zggcd (-x) y = 
-      let (p1,p) := Zggcd x y in
-      let (p2,p3) := p in
-       (p1,(-p2,p3))%Z.
- intros [|x|x] [|y|y]; unfold Zggcd, Zopp; auto.
- case Pggcd; intros p1 (p2, p3); auto.
- case Pggcd; intros p1 (p2, p3); auto.
- case Pggcd; intros p1 (p2, p3); auto.
- case Pggcd; intros p1 (p2, p3); auto.
- Qed.
-
- Theorem Zgcd_inv_0_l: forall x y, (Zgcd x y = 0)%Z -> x = 0%Z.
- intros x y H.
- assert (F1: (Zdivide 0 x)%Z).
-  rewrite <- H.
-  generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
- inversion F1 as[z H1].
- rewrite H1; ring.
- Qed.
-
- Theorem Zgcd_inv_0_r: forall x y, (Zgcd x y = 0)%Z -> y = 0%Z.
- intros x y H.
- assert (F1: (Zdivide 0 y)%Z).
-  rewrite <- H.
-  generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
- inversion F1 as[z H1].
- rewrite H1; ring.
- Qed.
-
- Theorem Zgcd_div: forall a b c,
-  (0 < c -> (c | b) -> (a * b)/c = a * (b/c))%Z.
- intros a b c H1 H2.
- inversion H2 as [z Hz].
- rewrite Hz; rewrite Zmult_assoc.
- repeat rewrite Z_div_mult; auto with zarith.
- Qed.
-
- Theorem Zgcd_div_swap a b c:
- (0 < Zgcd a b)%Z ->
- (0 < b)%Z ->
- (c * a / Zgcd a b * b)%Z = (c * a * (b/Zgcd a b))%Z.
- intros a b c Hg Hb.
- assert (F := (Zgcd_is_gcd a b)); inversion F as [F1 F2 F3].
- pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
- repeat rewrite Zmult_assoc.
- apply f_equal2 with (f := Zmult); auto.
- rewrite Zgcd_div; auto.
- rewrite <- Zmult_assoc.
- rewrite (fun x y => Zmult_comm (x /y)); 
-   rewrite <- (Zdivide_Zdiv_eq); auto.
- Qed.
 
+(* P.L. : See Numtheory.v *)
 
 (**************************************
   Properties rel_prime
@@ -810,7 +691,6 @@ rewrite <- H1; apply Zgcd_is_gcd.
 right; contradict H1.
 case (Zis_gcd_unique a b (Zgcd a b) 1); auto.
 apply Zgcd_is_gcd.
-apply Zis_gcd_sym; auto.
 intros H2; absurd (0 <= Zgcd a b); auto with zarith.
 generalize (Zgcd_is_pos a b); auto with zarith.
 Qed.
@@ -843,7 +723,6 @@ case (Zis_gcd_unique  0 n n 1); auto.
 apply Zis_gcd_intro; auto.
 exists 0; auto with zarith.
 exists 1; auto with zarith.
-apply Zis_gcd_sym; auto.
 Qed.
 
 Theorem rel_prime_mod: forall p q, 0 < q -> rel_prime p q -> rel_prime (p mod q) q.
@@ -889,7 +768,7 @@ intros H1; absurd (1 < 1); auto with zarith.
 inversion H1; auto.
 Qed.
  
-Theorem prime2: prime 2.
+Theorem prime_2: prime 2.
 apply prime_intro; auto with zarith.
 intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
  clear H1; intros H1.
@@ -898,7 +777,7 @@ subst n; red; auto with zarith.
 apply Zis_gcd_intro; auto with zarith.
 Qed.
  
-Theorem prime3: prime 3.
+Theorem prime_3: prime 3.
 apply prime_intro; auto with zarith.
 intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
  clear H1; intros H1.
@@ -1288,55 +1167,6 @@ rewrite Zpower_tr_aux_correct with (p := 0%nat); auto.
 Qed.
 
 
- Theorem Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.
- Proof.
- intros x; unfold Zpower_pos; simpl; ring.
- Qed.
-
- Theorem Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1%Z.
- Proof.
- intros p; elim p; clear p.
- intros p Hrec.
-   rewrite xI_succ_xO; rewrite <- Pplus_diag; rewrite Pplus_one_succ_l.
-   repeat rewrite Zpower_pos_is_exp.
-   rewrite Zpower_pos_1_r.
-   rewrite Hrec; ring.
- intros p Hrec.
-   rewrite <- Pplus_diag.
-   repeat rewrite Zpower_pos_is_exp.
-   rewrite Hrec; ring.
- rewrite Zpower_pos_1_r; auto.
- Qed.
-
-
-
- Theorem Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0%Z.
- intros p; elim p; clear p.
- intros p H1.
- change (xI p) with (1 + (xO p))%positive.
- rewrite Zpower_pos_is_exp; rewrite Zpower_pos_1_r; auto.
- intros p Hrec; rewrite <- Pplus_diag; 
-  rewrite Zpower_pos_is_exp; rewrite Hrec; auto.
- rewrite Zpower_pos_1_r; auto.
- Qed.
-
-
- Theorem Zpower_pos_pos: forall x p, 
-     (0 < x -> 0 < Zpower_pos x p)%Z.
- Proof.
- intros x p; elim p; clear p.
- intros p Hrec H0.
- rewrite xI_succ_xO; rewrite <- Pplus_diag; rewrite Pplus_one_succ_l.
-   repeat rewrite Zpower_pos_is_exp.
-   rewrite Zpower_pos_1_r.
-   repeat apply Zmult_lt_0_compat; auto.
- intros p Hrec H0.
- rewrite <- Pplus_diag.
-   repeat rewrite Zpower_pos_is_exp.
-   repeat apply Zmult_lt_0_compat; auto.
- rewrite Zpower_pos_1_r; auto.
- Qed.
-
 (************************************** 
   Definition of Zsquare 
 **************************************)
diff --git a/theories/Ints/num/Q0Make.v b/theories/Ints/num/Q0Make.v
index 09a060e421..326e629024 100644
--- a/theories/Ints/num/Q0Make.v
+++ b/theories/Ints/num/Q0Make.v
@@ -8,7 +8,7 @@ Require Export BigN.
 Require Export BigZ.
 Require Import QArith.
 Require Import Qcanon.
-Require Import QBAux.
+Require Import Qpower.
 Require Import QMake_base.
 
 Module Q0.
diff --git a/theories/Ints/num/QbiMake.v b/theories/Ints/num/QbiMake.v
index fe7d9cb25d..53fb65b2a8 100644
--- a/theories/Ints/num/QbiMake.v
+++ b/theories/Ints/num/QbiMake.v
@@ -8,7 +8,7 @@ Require Export BigN.
 Require Export BigZ.
 Require Import QArith.
 Require Import Qcanon.
-Require Import QBAux.
+Require Import Qpower.
 Require Import QMake_base.	
 
 Module Qbi.
diff --git a/theories/Ints/num/QifMake.v b/theories/Ints/num/QifMake.v
index 3ee0227766..add89898a8 100644
--- a/theories/Ints/num/QifMake.v
+++ b/theories/Ints/num/QifMake.v
@@ -8,7 +8,7 @@ Require Export BigN.
 Require Export BigZ.
 Require Import QArith.
 Require Import Qcanon.
-Require Import QBAux.
+Require Import Qpower.
 Require Import QMake_base.
 
 Module Qif.
diff --git a/theories/Ints/num/QpMake.v b/theories/Ints/num/QpMake.v
index 1ae9fa4ef3..3c859d0f12 100644
--- a/theories/Ints/num/QpMake.v
+++ b/theories/Ints/num/QpMake.v
@@ -8,7 +8,7 @@ Require Export BigN.
 Require Export BigZ.
 Require Import QArith.
 Require Import Qcanon.
-Require Import QBAux.
+Require Import Qpower.
 Require Import QMake_base.
 
 
diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v
index c223b6bd23..eb97123da3 100644
--- a/theories/Ints/num/QvMake.v
+++ b/theories/Ints/num/QvMake.v
@@ -8,7 +8,7 @@ Require Export BigN.
 Require Export BigZ.
 Require Import QArith.
 Require Import Qcanon.
-Require Import QBAux.
+Require Import Qpower.
 Require Import QMake_base.
 
 Module Qv.
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index d7486bc2bb..a910c89220 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -1226,6 +1226,24 @@ Proof.
   intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto.
 Qed.
 
+(** Number of digits in a number *)
+
+Fixpoint Psize (p:positive) : nat := 
+  match p with 
+    | xH => 1%nat
+    | xI p => S (Psize p) 
+    | xO p => S (Psize p)
+  end.
+
+Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat.
+Proof.
+  assert (le0 : forall n:nat, (0<=n)%nat) by (induction n; auto).
+  assert (leS : forall n m:nat, (n<=m)%nat -> (S n <= S m)%nat) by (induction 1; auto).
+  induction p; destruct q; simpl; auto; intros; try discriminate.
+  intros; generalize (Pcompare_Gt_Lt _ _ H); auto.
+  intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto.
+Qed.
+
 
 
 
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index cdb669bf66..04f454df4d 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -577,13 +577,6 @@ Qed.
 
 (** Number of digits in a number *)
 
-Fixpoint Psize (p:positive) : nat := 
-  match p with 
-    | xH => 1%nat
-    | xI p => S (Psize p) 
-    | xO p => S (Psize p)
-  end.
-
 Definition Nsize (n:N) : nat := match n with 
   | N0 => 0%nat
   | Npos p => Psize p
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 959a16c297..cfe0187a3f 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -547,4 +547,14 @@ auto.
 Qed.
 
 
-
+Theorem Qc_decomp: forall x y: Qc,
+  (Qred x = x -> Qred y = y -> (x:Q) = y)-> x = y.
+Proof.
+  intros (q, Hq) (q', Hq'); simpl; intros H.
+  assert (H1 := H Hq Hq').
+  subst q'.
+  assert (Hq = Hq'). 
+  apply Eqdep_dec.eq_proofs_unicity; auto; intros.
+  repeat decide equality.
+  congruence.
+Qed.
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index f837de4222..8fa680a729 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -1,4 +1,4 @@
-Require Import Qfield.
+Require Import Qfield Qreduction.
 
 Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1.
 Proof.
@@ -201,4 +201,33 @@ setoid_replace (a^2) with ((-a)*(-a)) by ring.
 rewrite Qle_minus_iff in A.
 setoid_replace (0+ - a) with (-a) in A by ring.
 apply Qmult_le_0_compat; assumption.
-Qed.
\ No newline at end of file
+Qed.
+
+Theorem Qpower_decomp: forall p x y,
+  Qpower_positive (x #y) p == x ^ Zpos p # (Z2P ((Zpos y) ^ Zpos p)).
+Proof.
+induction p; intros; unfold Qmult; simpl.
+(* xI *)
+rewrite IHp, xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
+repeat rewrite Zpower_pos_is_exp.
+red; unfold Qmult, Qnum, Qden, Zpower.
+repeat rewrite Zpos_mult_morphism.
+repeat rewrite Z2P_correct.
+repeat rewrite Zpower_pos_1_r; ring.
+apply Zpower_pos_pos; red; auto.
+repeat apply Zmult_lt_0_compat; auto;
+ apply Zpower_pos_pos; red; auto.
+(* xO *)
+rewrite IHp, <-Pplus_diag.
+repeat rewrite Zpower_pos_is_exp.
+red; unfold Qmult, Qnum, Qden, Zpower.
+repeat rewrite Zpos_mult_morphism.
+repeat rewrite Z2P_correct; try ring.
+apply Zpower_pos_pos; red; auto.
+repeat apply Zmult_lt_0_compat; auto;
+ apply Zpower_pos_pos; red; auto.
+(* xO *)
+unfold Qmult; simpl.
+red; simpl; rewrite Zpower_pos_1_r;
+ rewrite Zpos_mult_morphism; ring.
+Qed.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index ddd9b0a268..6b16cfff4c 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -177,3 +177,17 @@ Add Morphism Qminus' : Qminus'_comp.
   intros; unfold Qminus' in |- *.
   rewrite H; rewrite H0; auto with qarith.
 Qed.
+
+Lemma Qred_opp: forall q, Qred (-q) = - (Qred q).
+Proof.
+  intros (x, y); unfold Qred; simpl.
+  rewrite Zggcd_opp; case Zggcd; intros p1 (p2, p3); simpl.
+  unfold Qopp; auto.
+Qed.
+
+Theorem Qred_compare: forall x y,
+  Qcompare x y = Qcompare (Qred x) (Qred y).
+Proof.
+  intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct.
+Qed.
+
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 0d67f21153..4e8373f605 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -739,6 +739,16 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> 
+  Zpos (b-a) = Zpos b - Zpos a.
+Proof.
+  intros.
+  simpl.
+  change Eq with (CompOpp Eq).
+  rewrite <- Pcompare_antisym.
+  rewrite H; simpl; auto.
+Qed.
+
 (** ** Misc redundant properties *)
 
 Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 1ba774941f..262d7bac58 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -12,7 +12,6 @@ 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.
 
@@ -156,21 +155,27 @@ Qed.
 
 Lemma Zdivide_antisym : forall a b:Z, (a | b) -> (b | a) -> a = b \/ a = - b.
 Proof.
-simple induction 1; intros.
-inversion H1.
-rewrite H0 in H2; clear H H1.
-case (Z_zerop a); intro.
-left; rewrite H0; rewrite e; ring.
-assert (Hqq0 : q0 * q = 1).
-apply Zmult_reg_l with a.
-assumption.
-ring_simplify.
-pattern a at 2 in |- *; rewrite H2; ring.
-assert (q | 1).
-rewrite <- Hqq0; auto with zarith.
-elim (Zdivide_1 q H); intros.
-rewrite H1 in H0; left; omega.
-rewrite H1 in H0; right; omega.
+  simple induction 1; intros.
+  inversion H1.
+  rewrite H0 in H2; clear H H1.
+  case (Z_zerop a); intro.
+  left; rewrite H0; rewrite e; ring.
+  assert (Hqq0 : q0 * q = 1).
+  apply Zmult_reg_l with a.
+  assumption.
+  ring_simplify.
+  pattern a at 2 in |- *; rewrite H2; ring.
+  assert (q | 1).
+  rewrite <- Hqq0; auto with zarith.
+  elim (Zdivide_1 q H); intros.
+  rewrite H1 in H0; left; omega.
+  rewrite H1 in H0; right; omega.
+Qed.
+ 
+Theorem Zdivide_trans: forall a b c, (a | b) -> (b | c) ->  (a | c).
+Proof.
+  intros a b c [d H1] [e H2]; exists (d * e); auto with zarith.
+  rewrite H2; rewrite H1; ring.
 Qed.
 
 (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
@@ -194,6 +199,100 @@ Proof.
   subst q; omega.
 Qed.
 
+(** [Zdivide] can be expressed using [Zmod]. *)
+
+Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a).
+Proof.
+  intros a b H H0.
+  apply Zdivide_intro with (a / b).
+  pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H).
+  rewrite H0; ring.
+Qed.
+
+Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0.
+Proof.
+  intros a b; simple destruct 2; intros; subst.
+  change (q * b) with (0 + q * b) in |- *.
+  rewrite Z_mod_plus; auto.
+Qed.
+
+(** [Zdivide] is hence decidable *)
+
+Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}.
+Proof.
+  intros a b; elim (Ztrichotomy_inf a 0).
+  (* a<0 *)
+  intros H; elim H; intros. 
+  case (Z_eq_dec (b mod - a) 0).
+  left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith.
+  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
+  (* a=0 *)
+  case (Z_eq_dec b 0); intro.
+  left; subst; auto with zarith.
+  right; subst; intro H0; inversion H0; omega.
+  (* a>0 *)
+  intro H; case (Z_eq_dec (b mod a) 0).
+  left; apply Zmod_divide; auto with zarith.
+  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
+Qed.
+
+Theorem Zdivide_Zdiv_eq: forall a b : Z, 
+ 0 < a -> (a | b) ->  b = a * (b / a).
+Proof.
+  intros a b Hb Hc.
+  pattern b at 1; rewrite (Z_div_mod_eq b a); auto with zarith.
+  rewrite (Zdivide_mod b a); auto with zarith.
+Qed.
+
+Theorem Zdivide_Zdiv_eq_2: forall a b c : Z, 
+ 0 < a -> (a | b) -> (c * b)/a = c * (b / a).
+Proof.
+  intros a b c H1 H2.
+  inversion H2 as [z Hz].
+  rewrite Hz; rewrite Zmult_assoc.
+  repeat rewrite Z_div_mult; auto with zarith.
+Qed.
+ 
+Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) ->  (a | b).
+Proof.
+  intros a b [x H]; subst b.
+  pattern (Zabs a); apply Zabs_intro.
+  exists (- x); ring.
+  exists x; ring.
+Qed.
+ 
+Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) ->  (Zabs a | b).
+Proof.
+  intros a b [x H]; subst b.
+  pattern (Zabs a); apply Zabs_intro.
+  exists (- x);  ring.
+  exists x; ring.
+Qed.
+
+Theorem Zdivide_le: forall a b : Z, 
+ 0 <= a -> 0 < b -> (a | b) ->  a <= b.
+Proof.
+  intros a b H1 H2 [q H3]; subst b.
+  case (Zle_lt_or_eq 0 a); auto with zarith; intros H3.
+  case (Zle_lt_or_eq 0 q); auto with zarith.
+  apply (Zmult_le_0_reg_r a); auto with zarith.
+  intros H4; apply Zle_trans with (1 * a); auto with zarith.
+  intros H4; subst q; omega.
+Qed.
+
+Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, 
+ 1 < a -> 0 < b -> (a | b) ->  0 < b / a < b .
+Proof.
+  intros a b H1 H2 H3; split.
+  apply Zmult_lt_reg_r with a; auto with zarith.
+  rewrite (Zmult_comm (Zdiv b a)); rewrite <- Zdivide_Zdiv_eq; auto with zarith.
+  apply Zmult_lt_reg_r with a; auto with zarith.
+  repeat rewrite (fun x => Zmult_comm x a); auto with zarith.
+  rewrite <- Zdivide_Zdiv_eq; auto with zarith.
+  pattern b at 1; replace b with (1 * b); auto with zarith.
+  apply Zmult_lt_compat_r; auto with zarith.
+Qed.
+
 (** * Greatest common divisor (gcd). *)
    
 (** There is no unicity of the gcd; hence we define the predicate [gcd a b d] 
@@ -246,6 +345,18 @@ Proof.
 Qed.
 
 Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.
+ 
+Theorem Zis_gcd_unique: forall a b c d : Z, 
+ Zis_gcd a b c -> Zis_gcd a b d ->  c = d \/ c = (- d).
+Proof.
+intros a b c d H1 H2.
+inversion_clear H1 as [Hc1 Hc2 Hc3].
+inversion_clear H2 as [Hd1 Hd2 Hd3].
+assert (H3: Zdivide c d); auto.
+assert (H4: Zdivide d c); auto.
+apply Zdivide_antisym; auto.
+Qed.
+
 
 (** * Extended Euclid algorithm. *)
 
@@ -543,43 +654,6 @@ Qed.
 
 Hint Resolve prime_rel_prime: zarith.
 
-(** [Zdivide] can be expressed using [Zmod]. *)
-
-Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a).
-Proof.
-  intros a b H H0.
-  apply Zdivide_intro with (a / b).
-  pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H).
-  rewrite H0; ring.
-Qed.
-
-Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0.
-Proof.
-  intros a b; simple destruct 2; intros; subst.
-  change (q * b) with (0 + q * b) in |- *.
-  rewrite Z_mod_plus; auto.
-Qed.
-
-(** [Zdivide] is hence decidable *)
-
-Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}.
-Proof.
-  intros a b; elim (Ztrichotomy_inf a 0).
-  (* a<0 *)
-  intros H; elim H; intros. 
-  case (Z_eq_dec (b mod - a) 0).
-  left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith.
-  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
-  (* a=0 *)
-  case (Z_eq_dec b 0); intro.
-  left; subst; auto with zarith.
-  right; subst; intro H0; inversion H0; omega.
-  (* a>0 *)
-  intro H; case (Z_eq_dec (b mod a) 0).
-  left; apply Zmod_divide; auto with zarith.
-  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
-Qed.
-
 (** If a prime [p] divides [ab] then it divides either [a] or [b] *)
 
 Lemma prime_mult :
@@ -617,105 +691,34 @@ Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive :=
 	| 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
+	| 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.
 
 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.
+Close Scope positive_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.
+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.
 
 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.
@@ -758,12 +761,12 @@ Proof.
   assert (Psize (b-a) <= Psize b)%nat.
   apply Psize_monotone.
   change (Zpos (b-a) < Zpos b).
-  rewrite (Pminus_Zminus _ _ H1).
+  rewrite (Zpos_minus_morphism _ _ H1).
   assert (0 < Zpos a) by (compute; auto).
   omega.
   omega.  
   rewrite Zpos_xO; do 2 rewrite Zpos_xI.
-  rewrite Pminus_Zminus; auto.
+  rewrite Zpos_minus_morphism; auto.
   omega.
   (* a = xI, b = xI, compare = Gt *)
   apply Zis_gcd_for_euclid with 1.
@@ -775,13 +778,13 @@ Proof.
   assert (Psize (a-b) <= Psize a)%nat.
   apply Psize_monotone.
   change (Zpos (a-b) < Zpos a).
-  rewrite (Pminus_Zminus b a).
+  rewrite (Zpos_minus_morphism 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.
+  rewrite Zpos_minus_morphism; auto.
   omega.
   rewrite ZC4; rewrite H1; auto.
   (* a = xI, b = xO *)
@@ -840,6 +843,146 @@ Proof.
   apply Pgcd_correct.
 Qed.
 
+Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
+Proof.
+  intros x y; exists (Zgcd x y).
+  split; [apply Zgcd_is_gcd  | apply Zgcd_is_pos].
+Qed.
+
+Theorem Zdivide_Zgcd: forall p q r : Z, 
+ (p | q) -> (p | r) -> (p | Zgcd q r).
+Proof.
+  intros p q r H1 H2.
+  assert (H3: (Zis_gcd q r (Zgcd q r))).
+  apply Zgcd_is_gcd.
+  inversion_clear H3; auto.
+Qed.
+
+Theorem Zis_gcd_gcd: forall a b c : Z, 
+ 0 <= c ->  Zis_gcd a b c -> Zgcd a b = c.
+Proof.
+  intros a b c H1 H2.
+  case (Zis_gcd_uniqueness_apart_sign a b c (Zgcd a b)); auto.
+  apply Zgcd_is_gcd; auto.
+  case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; subst; auto.
+  intros H3; subst.
+  generalize (Zgcd_is_pos a b); auto with zarith.
+  case (Zgcd a b); simpl; auto; intros; discriminate.
+Qed.
+
+Theorem Zgcd_inv_0_l: forall x y, Zgcd x y = 0 -> x = 0.
+Proof.
+  intros x y H.
+  assert (F1: Zdivide 0 x).
+   rewrite <- H.
+   generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
+  inversion F1 as [z H1].
+  rewrite H1; ring.
+Qed.
+
+Theorem Zgcd_inv_0_r: forall x y, Zgcd x y = 0 -> y = 0.
+Proof.
+  intros x y H.
+  assert (F1: Zdivide 0 y).
+   rewrite <- H.
+   generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
+  inversion F1 as [z H1].
+  rewrite H1; ring.
+Qed.
+
+Theorem Zgcd_div_swap0 : forall a b : Z, 
+ 0 < Zgcd a b ->
+ 0 < b ->
+ (a / Zgcd a b) * b = a * (b/Zgcd a b).
+Proof.
+ intros a b Hg Hb.
+ assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
+ pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+ repeat rewrite Zmult_assoc; f_equal.
+ rewrite Zmult_comm.
+ rewrite <- Zdivide_Zdiv_eq; auto.
+Qed.
+
+Theorem Zgcd_div_swap : forall a b c : Z, 
+ 0 < Zgcd a b ->
+ 0 < b ->
+ (c * a) / Zgcd a b * b = c * a * (b/Zgcd a b).
+Proof.
+ intros a b c Hg Hb.
+ assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
+ pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+ repeat rewrite Zmult_assoc; f_equal.
+ rewrite Zdivide_Zdiv_eq_2; auto.
+ repeat rewrite <- Zmult_assoc; f_equal.
+ rewrite Zmult_comm.
+ rewrite <- Zdivide_Zdiv_eq; auto.
+Qed.
+
+
+(** A Generalized Gcd that also computes Bezout coefficients.
+   The algorithm is the same as for Zgcd. *)
+
+Open Scope positive_scope.
+
+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 Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b.
+
+Open Scope Z_scope.
+
+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 Pggcdn_gcdn : forall n a b, 
   fst (Pggcdn n a b) = Pgcdn n a b.
@@ -870,8 +1013,8 @@ 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).
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
 Proof.
   induction n.
   simpl; auto.
@@ -910,30 +1053,32 @@ 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).
+  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.
+Close Scope positive_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).
+  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.
 
-Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
+Theorem Zggcd_opp: forall x y, 
+  Zggcd (-x) y = let (p1,p) := Zggcd x y in
+                 let (p2,p3) := p in
+                 (p1,(-p2,p3)).
 Proof.
-  intros x y; exists (Zgcd x y).
-  split; [apply Zgcd_is_gcd  | apply Zgcd_is_pos].
+intros [|x|x] [|y|y]; unfold Zggcd, Zopp; auto.
+case Pggcd; intros p1 (p2, p3); auto.
+case Pggcd; intros p1 (p2, p3); auto.
+case Pggcd; intros p1 (p2, p3); auto.
+case Pggcd; intros p1 (p2, p3); auto.
 Qed.
-
-
-
-
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 4e08c726ea..a1963a9659 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -14,81 +14,114 @@ Require Import Omega.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
 
-Section section1.
-
 (** * Definition of powers over [Z]*)
 
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *) 
 
-  Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
-
-  (** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
-      [plus : nat->nat] and [Zmult : Z->Z] *)
-
-  Lemma Zpower_nat_is_exp :
-    forall (n m:nat) (z:Z),
-      Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
-  Proof.
-    intros; elim n;
-      [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
-	| unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
-	  apply Zmult_assoc ].
-  Qed.
-
-  (** This theorem shows that powers of unary and binary integers
-     are the same thing, modulo the function convert : [positive -> nat] *)
+Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
+
+(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
+    [plus : nat->nat] and [Zmult : Z->Z] *)
+
+Lemma Zpower_nat_is_exp :
+  forall (n m:nat) (z:Z),
+    Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
+Proof.
+  intros; elim n;
+   [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
+     | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
+       apply Zmult_assoc ].
+Qed.
+
+(** This theorem shows that powers of unary and binary integers
+   are the same thing, modulo the function convert : [positive -> nat] *)
+
+Theorem Zpower_pos_nat :
+  forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
+Proof.
+  intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
+    apply iter_nat_of_P.
+Qed.
+
+(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
+   deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
+   for [add : positive->positive] and [Zmult : Z->Z] *)
+
+Theorem Zpower_pos_is_exp :
+  forall (n m:positive) (z:Z),
+    Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
+Proof.
+  intros.
+  rewrite (Zpower_pos_nat z n).
+  rewrite (Zpower_pos_nat z m).
+  rewrite (Zpower_pos_nat z (n + m)).
+  rewrite (nat_of_P_plus_morphism n m).
+  apply Zpower_nat_is_exp.
+Qed.
+
+Theorem Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.
+Proof.
+  intros x; unfold Zpower_pos; simpl; auto with zarith.
+Qed.
+
+Theorem Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1.
+Proof.
+  induction p.
+  (* xI *)
+  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite Zpower_pos_1_r, IHp; auto.
+  (* xO *)
+  rewrite <- Pplus_diag.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite IHp; auto.
+  (* xH *)
+  rewrite Zpower_pos_1_r; auto.
+Qed.
+
+Theorem Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0.
+Proof. 
+  induction p.
+  change (xI p) with (1 + (xO p))%positive.
+  rewrite Zpower_pos_is_exp, Zpower_pos_1_r; auto.
+  rewrite <- Pplus_diag.
+  rewrite Zpower_pos_is_exp, IHp; auto.
+  rewrite Zpower_pos_1_r; auto.
+Qed.
+
+Theorem Zpower_pos_pos: forall x p, 
+  0 < x -> 0 < Zpower_pos x p.
+Proof.
+  induction p; intros.
+  (* xI *)
+  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite Zpower_pos_1_r.
+  repeat apply Zmult_lt_0_compat; auto.
+  (* xO *)
+  rewrite <- Pplus_diag.
+  repeat rewrite Zpower_pos_is_exp.
+  repeat apply Zmult_lt_0_compat; auto.
+  (* xH *)
+  rewrite Zpower_pos_1_r; auto.
+Qed.
 
-  Theorem Zpower_pos_nat :
-    forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
-  Proof.
-    intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
-      apply iter_nat_of_P.
-  Qed.
-
-  (** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
-     deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
-     for [add : positive->positive] and [Zmult : Z->Z] *)
-
-  Theorem Zpower_pos_is_exp :
-    forall (n m:positive) (z:Z),
-      Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
-  Proof.
-    intros.
-    rewrite (Zpower_pos_nat z n).
-    rewrite (Zpower_pos_nat z m).
-    rewrite (Zpower_pos_nat z (n + m)).
-    rewrite (nat_of_P_plus_morphism n m).
-    apply Zpower_nat_is_exp.
-  Qed.
-
-  Infix "^" := Zpower : Z_scope.
-
-  Hint Immediate Zpower_nat_is_exp: zarith.
-  Hint Immediate Zpower_pos_is_exp: zarith.
-  Hint Unfold Zpower_pos: zarith.
-  Hint Unfold Zpower_nat: zarith.
-
-  Lemma Zpower_exp :
-    forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
-  Proof.
-    destruct n; destruct m; auto with zarith.
-    simpl in |- *; intros; apply Zred_factor0.
-    simpl in |- *; auto with zarith.
-    intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
-    intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
-  Qed.
-
-End section1.
+Infix "^" := Zpower : Z_scope.
 
-(** Exporting notation "^" *)
+Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
+Hint Unfold Zpower_pos Zpower_nat: zarith.
 
-Infix "^" := Zpower : Z_scope.
+Lemma Zpower_exp :
+  forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
+Proof.
+  destruct n; destruct m; auto with zarith.
+  simpl in |- *; intros; apply Zred_factor0.
+  simpl in |- *; auto with zarith.
+  intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
+  intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
+Qed.
 
-Hint Immediate Zpower_nat_is_exp: zarith.
-Hint Immediate Zpower_pos_is_exp: zarith.
-Hint Unfold Zpower_pos: zarith.
-Hint Unfold Zpower_nat: zarith.
 
 Section Powers_of_2.