1 files changed, 596 insertions, 154 deletions

diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index d89ec052..e77475e0 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -6,13 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Znumtheory.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Znumtheory.v 10295 2007-11-06 22:46:21Z letouzey $ i*)
 
 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,134 @@ 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.
+
+Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m ->
+ (n | m) -> a mod n = (a mod m) mod n.
+Proof.
+  intros n m a H1 H2 H3.
+  pattern a at 1; rewrite (Z_div_mod_eq a m); auto with zarith.
+  case H3; intros q Hq; pattern m at 1; rewrite Hq.
+  rewrite (Zmult_comm q).
+  rewrite Zplus_mod; auto with zarith.
+  rewrite <- Zmult_assoc; rewrite Zmult_mod; auto with zarith.
+  rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith.
+  rewrite (Zmod_small 0); auto with zarith.
+  rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith.
+Qed.
+
+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.
+  rewrite Zminus_mod; auto with zarith.
+  rewrite H1; pattern c at 1; rewrite <- (Zmod_small c b); auto with zarith.
+  rewrite Zminus_diag; apply Zmod_small; auto with zarith.
+  subst; apply Z_mod_lt; auto with zarith.
+Qed.
+
+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.
+  replace a with ((a - c) + c); auto with zarith.
+  rewrite Zplus_mod; auto with zarith.
+  rewrite (Zdivide_mod (a -c) b); try rewrite Zplus_0_l; auto with zarith.
+  rewrite Zmod_mod; try apply Zmod_small; 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 +379,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. *)
 
@@ -463,6 +608,7 @@ Qed.
 Lemma Zis_gcd_rel_prime :
   forall a b g:Z,
     b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g).
+Proof.
   intros a b g; intros.
   assert (g <> 0).
   intro.
@@ -491,6 +637,68 @@ Lemma Zis_gcd_rel_prime :
   exists q; auto with zarith.
 Qed.
 
+Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a.
+Proof.
+  intros a b H; auto with zarith.
+  red; apply Zis_gcd_sym; auto with zarith.
+Qed.
+
+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.
+  inversion_clear H as [H1 H2 H3].
+  red; apply Zis_gcd_intro; try apply Zone_divide.
+  intros x H4 H5; apply H3; auto.
+  apply Zdivide_mult_r; auto.
+Qed.
+
+Theorem rel_prime_1: forall n, rel_prime 1 n.
+Proof.
+  intros n; red; apply Zis_gcd_intro; auto.
+  exists 1; auto with zarith.
+  exists n; auto with zarith.
+Qed.
+
+Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.
+Proof.
+  intros n H H1; absurd (n = 1 \/ n = -1).
+  intros [H2 | H2]; subst; contradict H; auto with zarith.
+  case (Zis_gcd_unique  0 n n 1); auto.
+  apply Zis_gcd_intro; auto.
+  exists 0; auto with zarith.
+  exists 1; auto with zarith.
+Qed.
+
+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.
+  assert (H1: Bezout p q 1).
+  apply rel_prime_bezout; auto.
+  inversion_clear H1 as [q1 r1 H2].
+  apply bezout_rel_prime.
+  apply Bezout_intro with q1  (r1 + q1 * (p / q)).
+  rewrite <- H2.
+  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 -> 
+ rel_prime (p mod q) q -> rel_prime p q.
+Proof.
+  intros p q H H0.
+  rewrite (Z_div_mod_eq p q); auto with zarith; red.
+  apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto with zarith.
+Qed.
+
+Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0.
+Proof.
+  intros a b H H1 H2.
+  case (not_rel_prime_0 _ H).
+  rewrite <- H2.
+  apply rel_prime_mod; auto with zarith.
+Qed.
+
 (** * Primality *)
 
 Inductive prime (p:Z) : Prop :=
@@ -543,42 +751,19 @@ Qed.
 
 Hint Resolve prime_rel_prime: zarith.
 
-(** [Zdivide] can be expressed using [Zmod]. *)
+(** As a consequence, a prime number is relatively prime with smaller numbers *)
 
-Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a).
+Theorem rel_prime_le_prime:
+ forall a p, prime p -> 1 <=  a < p -> rel_prime a p.
 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 p Hp [H1 H2].
+  apply rel_prime_sym; apply prime_rel_prime; auto.
+  intros [q Hq]; subst a.
+  case (Zle_or_lt q 0); intros Hl.
+  absurd (q * p <= 0 * p); auto with zarith.
+  absurd (1 * p <= q * p); auto with zarith.
 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] *)
 
@@ -590,6 +775,108 @@ Proof.
   right; apply Gauss with a; auto with zarith.
 Qed.
 
+Lemma not_prime_0: ~ prime 0.
+Proof.
+  intros H1; case (prime_divisors _ H1 2); auto with zarith.
+Qed.
+
+Lemma not_prime_1: ~ prime 1.
+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.
+  intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
+   clear H1; intros H1.
+  contradict H2; auto with zarith.
+  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.
+  intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
+   clear H1; intros H1.
+  case (Zle_lt_or_eq 2 n); auto with zarith; clear H1; intros H1.
+  contradict H2; auto with zarith.
+  subst n; red; auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+  intros x [q1 Hq1] [q2 Hq2].
+  exists (q2 - q1).
+  apply trans_equal with (3 - 2); auto with zarith.
+  rewrite Hq1; rewrite Hq2; ring.
+  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.
+Qed.
+
+Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)).
+
+Theorem prime_alt: 
+ forall p, prime' p <-> prime p.
+Proof.
+  split; destruct 1; intros.
+  (* prime -> prime' *)
+  constructor; auto; intros.
+  red; apply Zis_gcd_intro; auto with zarith; intros.
+  case (Zle_lt_or_eq 0 (Zabs x)); auto with zarith; intros H6.
+  case (Zle_lt_or_eq 1 (Zabs x)); auto with zarith; intros H7.
+  case (Zle_lt_or_eq (Zabs x) p); auto with zarith.
+  apply Zdivide_le; auto with zarith.
+  apply Zdivide_Zabs_inv_l; auto.
+  intros H8; case (H0 (Zabs x)); auto.
+  apply Zdivide_Zabs_inv_l; auto.
+  intros H8; subst p; absurd (Zabs x <= n); auto with zarith.
+  apply Zdivide_le; auto with zarith.
+  apply Zdivide_Zabs_inv_l; auto.
+  rewrite H7; pattern (Zabs x); apply Zabs_intro; auto with zarith.
+  absurd (0%Z = p); auto with zarith.
+  assert (x=0) by (destruct x; simpl in *; now auto).
+  subst x; elim H3; intro q; rewrite Zmult_0_r; auto.
+  (* prime' -> prime *)
+  split; auto; intros.
+  intros H2.
+  case (Zis_gcd_unique n p n 1); auto with zarith.
+  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.
+  rewrite <- (Zabs_square a) in Ha.
+  assert (0 <= Zabs a) by auto with zarith.
+  set (b:=Zabs a) in *; clearbody b.
+  rewrite <- prime_alt in Ha; destruct Ha.
+  case (Zle_lt_or_eq 0 b); auto with zarith; intros Hza1; [ | subst; omega].
+  case (Zle_lt_or_eq 1 b); auto with zarith; intros Hza2; [ | subst; omega].
+  assert (Hza3 := Zmult_lt_compat_r 1 b b Hza1 Hza2).
+  rewrite Zmult_1_l in Hza3.
+  elim (H1 _ (conj Hza2 Hza3)).
+  exists b; auto.
+Qed.
+
+Theorem prime_div_prime: forall p q, 
+ prime p -> prime q -> (p | q) -> p = q.
+Proof.
+  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.
+  intros H4; contradict Hp; subst; auto with zarith.
+  intros [H4| [H4 | H4]]; subst; auto.
+  contradict H; auto; apply not_prime_1.
+  contradict Hp; auto with zarith.
+Qed.
+
 
 (** We could obtain a [Zgcd] function via Euclid algorithm. But we propose 
   here a binary version of [Zgcd], faster and executable within Coq.
@@ -617,105 +904,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 +974,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 +991,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 +1056,230 @@ 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.
+
+Theorem Zgcd_1_rel_prime : forall a b, 
+ Zgcd a b = 1 <-> rel_prime a b.
+Proof.
+  unfold rel_prime; split; intro H.
+  rewrite <- H; apply Zgcd_is_gcd.
+  case (Zis_gcd_unique a b (Zgcd a b) 1); auto.
+  apply Zgcd_is_gcd.
+  intros H2; absurd (0 <= Zgcd a b); auto with zarith.
+  generalize (Zgcd_is_pos a b); auto with zarith.
+Qed.
+
+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.
+  left; apply -> Zgcd_1_rel_prime; auto.
+  right; contradict H1; apply <- Zgcd_1_rel_prime; auto.
+Defined.
+
+Definition prime_dec_aux:
+ forall p m,
+  { forall n, 1 < n < m -> rel_prime n p } +
+  { 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 ].
+  pattern m; apply natlike_rec; auto with zarith.
+  left; intros; elimtype False; omega.
+  intros x Hx IH; destruct IH as [F|E].
+  destruct (rel_prime_dec x p) as [Y|N].
+  left; intros n [HH1 HH2].
+  case (Zgt_succ_gt_or_eq x n); auto with zarith.
+  intros HH3; subst x; auto.
+  case (Z_lt_dec 1 x); intros HH1.
+  right; exists x; split; auto with zarith.
+  left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith.
+  right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith.
+Defined.
+
+Definition prime_dec: forall p, { prime p }+{ ~ prime p }.
+Proof.
+  intros p; case (Z_lt_dec 1 p); intros H1.
+  case (prime_dec_aux p p); intros H2.
+  left; apply prime_intro; auto.
+  intros n [Hn1 Hn2]; case Zle_lt_or_eq with ( 1 := Hn1 ); auto.
+  intros HH; subst n.
+  red; apply Zis_gcd_intro; auto with zarith.
+  right; intros H3; inversion_clear H3 as [Hp1 Hp2].
+  case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith.
+  right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto.
+Defined.
+
+Theorem not_prime_divide:
+ forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p  /\ (n | p).
+Proof.
+  intros p Hp Hp1.
+  case (prime_dec_aux p p); intros H1.
+  elim Hp1; constructor; auto.
+  intros n [Hn1 Hn2].
+  case Zle_lt_or_eq with ( 1 := Hn1 ); auto with zarith.
+  intros H2; subst n; red; apply Zis_gcd_intro; auto with zarith.
+  case H1; intros n [Hn1 Hn2].
+  generalize (Zgcd_is_pos n p); intros Hpos.
+  case (Zle_lt_or_eq 0 (Zgcd n p)); auto with zarith; intros H3.
+  case (Zle_lt_or_eq 1 (Zgcd n p)); auto with zarith; intros H4.
+  exists (Zgcd n p); split; auto.
+  split; auto.
+  apply Zle_lt_trans with n; auto with zarith.
+  generalize (Zgcd_is_gcd n p); intros tmp; inversion_clear tmp as [Hr1 Hr2 Hr3].
+  case Hr1; intros q Hq.
+  case (Zle_or_lt q 0); auto with zarith; intros Ht.
+  absurd (n <= 0 * Zgcd n p) ; auto with zarith.
+  pattern n at 1; rewrite Hq; auto with zarith.
+  apply Zle_trans with (1 * Zgcd n p); auto with zarith.
+  pattern n at 2; rewrite Hq; auto with zarith.
+  generalize (Zgcd_is_gcd n p); intros Ht; inversion Ht; auto.
+  case Hn2; red.
+  rewrite H4; apply Zgcd_is_gcd.
+  generalize (Zgcd_is_gcd n p); rewrite <- H3; intros tmp;
+  inversion_clear tmp as [Hr1 Hr2 Hr3].
+  absurd (n = 0); auto with zarith.
+  case Hr1; auto with zarith.
+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 +1310,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 +1350,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.
-
-
-
-