Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 153 insertions, 119 deletions

diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 9be372a3..2a2751c9 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Znumtheory.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id$ i*)
 
 Require Import ZArith_base.
 Require Import ZArithRing.
@@ -15,13 +15,13 @@ Require Import Zdiv.
 Require Import Wf_nat.
 Open Local Scope Z_scope.
 
-(** This file contains some notions of number theory upon Z numbers: 
+(** This file contains some notions of number theory upon Z numbers:
      - a divisibility predicate [Zdivide]
      - a gcd predicate [gcd]
      - Euclid algorithm [euclid]
      - a relatively prime predicate [rel_prime]
      - a prime predicate [prime]
-     - an efficient [Zgcd] function 
+     - an efficient [Zgcd] function
 *)
 
 (** * Divisibility *)
@@ -171,7 +171,7 @@ Proof.
   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.
@@ -201,19 +201,17 @@ Qed.
 
 (** [Zdivide] can be expressed using [Zmod]. *)
 
-Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a).
+Lemma Zmod_divide : forall a b, 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.
+ intros a b NZ EQ.
+ apply Zdivide_intro with (a/b).
+ rewrite (Z_div_mod_eq_full a b NZ) at 1.
+ rewrite EQ; ring.
 Qed.
 
-Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0.
+Lemma Zdivide_mod : forall a b, (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.
+  intros a b (c,->); apply Z_mod_mult.
 Qed.
 
 (** [Zdivide] is hence decidable *)
@@ -222,7 +220,7 @@ 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. 
+  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.
@@ -236,7 +234,7 @@ Proof.
   intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
 Qed.
 
-Theorem Zdivide_Zdiv_eq: forall a b : Z, 
+Theorem Zdivide_Zdiv_eq: forall a b : Z,
  0 < a -> (a | b) ->  b = a * (b / a).
 Proof.
   intros a b Hb Hc.
@@ -244,7 +242,7 @@ Proof.
   rewrite (Zdivide_mod b a); auto with zarith.
 Qed.
 
-Theorem Zdivide_Zdiv_eq_2: forall a b c : Z, 
+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.
@@ -252,7 +250,7 @@ Proof.
   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.
@@ -260,7 +258,7 @@ Proof.
   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.
@@ -269,7 +267,7 @@ Proof.
   exists x; ring.
 Qed.
 
-Theorem Zdivide_le: forall a b : Z, 
+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.
@@ -280,7 +278,7 @@ Proof.
   intros H4; subst q; omega.
 Qed.
 
-Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, 
+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.
@@ -307,7 +305,7 @@ Proof.
   rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith.
 Qed.
 
-Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> 
+Lemma 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.
@@ -317,7 +315,7 @@ Proof.
   subst; apply Z_mod_lt; auto with zarith.
 Qed.
 
-Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b -> 
+Lemma 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.
@@ -328,9 +326,9 @@ Proof.
 Qed.
 
 (** * Greatest common divisor (gcd). *)
-   
-(** There is no unicity of the gcd; hence we define the predicate [gcd a b d] 
-     expressing that [d] is a gcd of [a] and [b]. 
+
+(** There is no unicity of the gcd; hence we define the predicate [gcd a b d]
+     expressing that [d] is a gcd of [a] and [b].
      (We show later that the [gcd] is actually unique if we discard its sign.) *)
 
 Inductive Zis_gcd (a b d:Z) : Prop :=
@@ -379,8 +377,8 @@ 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, 
+
+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.
@@ -431,7 +429,7 @@ Section extended_euclid_algorithm.
   (** The recursive part of Euclid's algorithm uses well-founded
       recursion of non-negative integers. It maintains 6 integers
       [u1,u2,u3,v1,v2,v3] such that the following invariant holds:
-      [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. 
+      [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)].
       *)
 
   Lemma euclid_rec :
@@ -455,8 +453,8 @@ Section extended_euclid_algorithm.
     replace (u3 - q * x) with (u3 mod x).
     apply Z_mod_lt; omega.
     assert (xpos : x > 0). omega.
-    generalize (Z_div_mod_eq u3 x xpos). 
-    unfold q in |- *. 
+    generalize (Z_div_mod_eq u3 x xpos).
+    unfold q in |- *.
     intro eq; pattern u3 at 2 in |- *; rewrite eq; ring.
     apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)).
     tauto.
@@ -531,7 +529,7 @@ Proof.
   rewrite H6; rewrite H7; ring.
   ring.
 Qed.
-  
+
 
 (** * Relative primality *)
 
@@ -612,16 +610,16 @@ Proof.
   intros a b g; intros.
   assert (g <> 0).
   intro.
-  elim H1; intros. 
+  elim H1; intros.
   elim H4; intros.
   rewrite H2 in H6; subst b; omega.
   unfold rel_prime in |- *.
   destruct H1.
   destruct H1 as (a',H1).
   destruct H3 as (b',H3).
-  replace (a/g) with a'; 
+  replace (a/g) with a';
     [|rewrite H1; rewrite Z_div_mult; auto with zarith].
-  replace (b/g) with b'; 
+  replace (b/g) with b';
     [|rewrite H3; rewrite Z_div_mult; auto with zarith].
   constructor.
   exists a'; auto with zarith.
@@ -643,7 +641,7 @@ Proof.
   red; apply Zis_gcd_sym; auto with zarith.
 Qed.
 
-Theorem rel_prime_div: forall p q r, 
+Theorem rel_prime_div: forall p q r,
  rel_prime p q -> (r | p) -> rel_prime r q.
 Proof.
   intros p q r H (u, H1); subst.
@@ -670,7 +668,7 @@ Proof.
   exists 1; auto with zarith.
 Qed.
 
-Theorem rel_prime_mod: forall p q, 0 < q -> 
+Theorem rel_prime_mod: forall p q, 0 < q ->
  rel_prime p q -> rel_prime (p mod q) q.
 Proof.
   intros p q H H0.
@@ -683,7 +681,7 @@ Proof.
   pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith.
 Qed.
 
-Theorem rel_prime_mod_rev: forall p q, 0 < q -> 
+Theorem rel_prime_mod_rev: forall p q, 0 < q ->
  rel_prime (p mod q) q -> rel_prime p q.
 Proof.
   intros p q H H0.
@@ -715,7 +713,7 @@ Proof.
   assert
     (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p).
   assert (Zabs a <= Zabs p). apply Zdivide_bounds; [ assumption | omega ].
-  generalize H3. 
+  generalize H3.
   pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *;
     apply Zabs_ind; intros; omega.
   intuition idtac.
@@ -785,7 +783,7 @@ Proof.
   intros H1; absurd (1 < 1); auto with zarith.
   inversion H1; auto.
 Qed.
- 
+
 Lemma prime_2: prime 2.
 Proof.
   apply prime_intro; auto with zarith.
@@ -795,7 +793,7 @@ Proof.
   subst n; red; auto with zarith.
   apply Zis_gcd_intro; auto with zarith.
 Qed.
- 
+
 Theorem prime_3: prime 3.
 Proof.
   apply prime_intro; auto with zarith.
@@ -812,7 +810,7 @@ Proof.
   subst n; red; auto with zarith.
   apply Zis_gcd_intro; auto with zarith.
 Qed.
- 
+
 Theorem prime_ge_2: forall p, prime p ->  2 <= p.
 Proof.
   intros p Hp; inversion Hp; auto with zarith.
@@ -820,7 +818,7 @@ Qed.
 
 Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)).
 
-Theorem prime_alt: 
+Theorem prime_alt:
  forall p, prime' p <-> prime p.
 Proof.
   split; destruct 1; intros.
@@ -848,7 +846,7 @@ Proof.
   apply Zis_gcd_intro; auto with zarith.
   apply H0; auto with zarith.
 Qed.
- 
+
 Theorem square_not_prime: forall a, ~ prime (a * a).
 Proof.
   intros a Ha.
@@ -864,10 +862,10 @@ Proof.
   exists b; auto.
 Qed.
 
-Theorem prime_div_prime: forall p q, 
+Theorem prime_div_prime: forall p q,
  prime p -> prime q -> (p | q) -> p = q.
 Proof.
-  intros p q H H1 H2; 
+  intros p q H H1 H2;
   assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
   assert (Hq: 0 < q); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
   case prime_divisors with (2 := H2); auto.
@@ -878,10 +876,10 @@ Proof.
 Qed.
 
 
-(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose 
+(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose
   here a binary version of [Zgcd], faster and executable within Coq.
 
-   Algorithm: 
+   Algorithm:
 
    gcd 0 b = b
    gcd a 0 = a
@@ -889,23 +887,23 @@ Qed.
    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 
-*)   
+                    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 
+Fixpoint Pgcdn (n: nat) (a b : positive) : positive :=
+  match n with
     | O => 1
-    | S n => 
-      match a,b with 
-	| xH, _ => 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 
+	| xI a', xI b' =>
+          match Pcompare a' b' Eq with
 	    | Eq => a
 	    | Lt => Pgcdn  n (b'-a') a
 	    | Gt => Pgcdn n (a'-b') b
@@ -919,7 +917,7 @@ Close Scope positive_scope.
 
 Definition Zgcd (a b : Z) : Z :=
   match a,b with
-    | Z0, _ => Zabs b 
+    | Z0, _ => Zabs b
     | _, Z0 => Zabs a
     | Zpos a, Zpos b => Zpos (Pgcd a b)
     | Zpos a, Zneg b => Zpos (Pgcd a b)
@@ -932,8 +930,8 @@ Proof.
   unfold Zgcd; destruct a; destruct b; auto with zarith.
 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. 
+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.
@@ -951,7 +949,7 @@ Proof.
   omega.
 Qed.
 
-Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> 
+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.
@@ -977,7 +975,7 @@ Proof.
   rewrite (Zpos_minus_morphism _ _ H1).
   assert (0 < Zpos a) by (compute; auto).
   omega.
-  omega.  
+  omega.
   rewrite Zpos_xO; do 2 rewrite Zpos_xI.
   rewrite Zpos_minus_morphism; auto.
   omega.
@@ -995,7 +993,7 @@ Proof.
   assert (0 < Zpos b) by (compute; auto).
   omega.
   rewrite ZC4; rewrite H1; auto.
-  omega.  
+  omega.
   rewrite Zpos_xO; do 2 rewrite Zpos_xI.
   rewrite Zpos_minus_morphism; auto.
   omega.
@@ -1062,7 +1060,7 @@ Proof.
   split; [apply Zgcd_is_gcd  | apply Zgcd_is_pos].
 Qed.
 
-Theorem Zdivide_Zgcd: forall p q r : Z, 
+Theorem Zdivide_Zgcd: forall p q r : Z,
  (p | q) -> (p | r) -> (p | Zgcd q r).
 Proof.
   intros p q r H1 H2.
@@ -1071,7 +1069,7 @@ Proof.
   inversion_clear H3; auto.
 Qed.
 
-Theorem Zis_gcd_gcd: forall a b c : Z, 
+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.
@@ -1103,7 +1101,7 @@ Proof.
   rewrite H1; ring.
 Qed.
 
-Theorem Zgcd_div_swap0 : forall a b : Z, 
+Theorem Zgcd_div_swap0 : forall a b : Z,
  0 < Zgcd a b ->
  0 < b ->
  (a / Zgcd a b) * b = a * (b/Zgcd a b).
@@ -1116,7 +1114,7 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
-Theorem Zgcd_div_swap : forall a b c : Z, 
+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).
@@ -1131,7 +1129,43 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
-Theorem Zgcd_1_rel_prime : forall a b, 
+Lemma Zgcd_comm : forall a b, Zgcd a b = Zgcd b a.
+Proof.
+  intros.
+  apply Zis_gcd_gcd.
+  apply Zgcd_is_pos.
+  apply Zis_gcd_sym.
+  apply Zgcd_is_gcd.
+Qed.
+
+Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
+Proof.
+  intros.
+  apply Zis_gcd_gcd.
+  apply Zgcd_is_pos.
+  destruct (Zgcd_is_gcd a b).
+  destruct (Zgcd_is_gcd b c).
+  destruct (Zgcd_is_gcd a (Zgcd b c)).
+  constructor; eauto using Zdivide_trans.
+Qed.
+
+Lemma Zgcd_Zabs : forall a b, Zgcd (Zabs a) b = Zgcd a b.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zgcd_0 : forall a, Zgcd a 0 = Zabs a.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zgcd_1 : forall a, Zgcd a 1 = 1.
+Proof.
+  intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
+Qed.
+Hint Resolve Zgcd_0 Zgcd_1 : zarith.
+
+Theorem Zgcd_1_rel_prime : forall a b,
  Zgcd a b = 1 <-> rel_prime a b.
 Proof.
   unfold rel_prime; split; intro H.
@@ -1142,7 +1176,7 @@ Proof.
   generalize (Zgcd_is_pos a b); auto with zarith.
 Qed.
 
-Definition rel_prime_dec: forall a b, 
+Definition rel_prime_dec: forall a b,
  { rel_prime a b }+{ ~ rel_prime a b }.
 Proof.
   intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1.
@@ -1156,10 +1190,10 @@ Definition prime_dec_aux:
   { exists n, 1 < n < m  /\ ~ rel_prime n p }.
 Proof.
   intros p m.
-  case (Z_lt_dec 1 m); intros H1; 
-   [ | left; intros; elimtype False; omega ].
+  case (Z_lt_dec 1 m); intros H1;
+   [ | left; intros; exfalso; omega ].
   pattern m; apply natlike_rec; auto with zarith.
-  left; intros; elimtype False; omega.
+  left; intros; exfalso; omega.
   intros x Hx IH; destruct IH as [F|E].
   destruct (rel_prime_dec x p) as [Y|N].
   left; intros n [HH1 HH2].
@@ -1221,34 +1255,34 @@ Qed.
 
 Open Scope positive_scope.
 
-Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := 
-  match n with 
+Fixpoint Pggcdn (n: nat) (a b : positive) : (positive*(positive*positive)) :=
+  match n with
     | O => (1,(a,b))
-    | S n => 
-      match a,b with 
-	| xH, b => (1,(1,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 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 
+	| 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 
+	| 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 
+	| 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 
+	     | 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 
+	     | Gt =>
+		let (g,p) := Pggcdn n (a'-b') b in
+		let (ab,bb) := p in
 		(g,(bb+xO ab, bb))
 	   end
       end
@@ -1260,28 +1294,28 @@ Open Scope Z_scope.
 
 Definition Zggcd (a b : Z) : Z*(Z*Z) :=
   match a,b with
-    | Z0, _ => (Zabs b,(0, Zsgn b)) 
+    | 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 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 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 
+    | 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 
+       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, 
+Lemma Pggcdn_gcdn : forall n a b,
   fst (Pggcdn n a b) = Pgcdn n a b.
 Proof.
   induction n.
@@ -1302,15 +1336,15 @@ 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 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 
+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.
@@ -1337,7 +1371,7 @@ Proof.
   rewrite <- H1; rewrite <- H0.
   simpl; f_equal; symmetry.
   apply Pplus_minus; auto.
-  (* Then... *) 
+  (* 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.
@@ -1348,9 +1382,9 @@ Proof.
   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 
+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).
@@ -1358,17 +1392,17 @@ Qed.
 
 Close Scope positive_scope.
 
-Lemma Zggcd_correct_divisors : forall a b, 
-  let (g,p) := Zggcd a b in 
-  let (aa,bb):=p in 
+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 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 Zggcd_opp: forall x y, 
+Theorem Zggcd_opp: forall x y,
   Zggcd (-x) y = let (p1,p) := Zggcd x y in
                  let (p2,p3) := p in
                  (p1,(-p2,p3)).