Import coqprime; use it to prove Euler's criterion.

4 files changed, 1433 insertions, 0 deletions

diff --git a/coqprime/Z/Pmod.v b/coqprime/Z/Pmod.v
new file mode 100644
index 000000000..f64af48e3
--- /dev/null
+++ b/coqprime/Z/Pmod.v
@@ -0,0 +1,617 @@
+
+(*************************************************************)
+(*      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      *)
+(*************************************************************)
+
+Require Export ZArith.
+Require Export ZCmisc.
+
+Open Local Scope positive_scope.
+
+Open Local Scope P_scope.
+
+(* [div_eucl a b] return [(q,r)] such that a = q*b + r *)
+Fixpoint div_eucl (a b : positive) {struct a} : N * N :=
+  match a with
+  | xH => if 1 ?< b then (0%N, 1%N) else (1%N, 0%N)
+  | xO a' =>
+    let (q, r) := div_eucl a' b in
+    match q, r with
+    | N0, N0 => (0%N, 0%N) (* n'arrive jamais *)
+    | N0, Npos r =>
+      if (xO r) ?< b then (0%N, Npos (xO r))
+      else (1%N,PminusN (xO r) b)
+    | Npos q, N0 => (Npos (xO q), 0%N)
+    | Npos q, Npos r =>
+      if (xO r) ?< b then (Npos (xO q), Npos (xO r))
+      else (Npos (xI q),PminusN (xO r) b)
+    end
+  | xI a' =>
+    let (q, r) := div_eucl a' b in
+    match q, r with
+    | N0, N0 => (0%N, 0%N)                 (* Impossible *)
+    | N0, Npos r =>  
+      if (xI r) ?< b then (0%N, Npos (xI r))
+      else (1%N,PminusN (xI r) b)
+    | Npos q, N0 => if 1 ?< b then (Npos (xO q), 1%N) else (Npos (xI q), 0%N)
+    | Npos q, Npos r => 
+      if (xI r) ?< b then (Npos (xO q), Npos (xI r))
+      else (Npos (xI q),PminusN (xI r) b)
+    end
+  end.
+Infix "/" := div_eucl : P_scope.
+
+Open Scope Z_scope.
+Opaque Zmult.
+Lemma div_eucl_spec : forall a b, 
+          Zpos a = fst (a/b)%P * b + snd (a/b)%P
+       /\ snd (a/b)%P < b.
+Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). 
+ intros a b;generalize a;clear a;induction a;simpl;zsimpl.
+ case IHa; destruct (a/b)%P as [q r].
+   case q; case r; simpl fst; simpl snd.
+     rewrite Zmult_0_l; rewrite Zplus_0_r; intros HH; discriminate HH.
+  intros p H; rewrite H;
+  match goal with 
+  | [|- context [ ?xx ?< b ]] => 
+    generalize (is_lt_spec xx b);destruct (xx ?< b)
+  | _ => idtac
+  end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto.
+  rewrite PminusN_le...
+  generalize H1; zsimpl; auto.
+  rewrite PminusN_le...
+  generalize H1; zsimpl; auto.
+  intros p H; rewrite H;
+  match goal with 
+  | [|- context [ ?xx ?< b ]] => 
+    generalize (is_lt_spec xx b);destruct (xx ?< b)
+  | _ => idtac
+  end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring.
+  ring_simplify.
+  case (Zle_lt_or_eq _ _ H1); auto with zarith.
+  intros p p1 H; rewrite H.
+  match goal with 
+  | [|- context [ ?xx ?< b ]] => 
+    generalize (is_lt_spec xx b);destruct (xx ?< b)
+  | _ => idtac
+  end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring.
+  rewrite PminusN_le...
+  generalize H1; zsimpl; auto.
+  rewrite PminusN_le...
+  generalize H1; zsimpl; auto.
+ case IHa; destruct (a/b)%P as [q r].
+   case q; case r; simpl fst; simpl snd.
+     rewrite Zmult_0_l; rewrite Zplus_0_r; intros HH; discriminate HH.
+  intros p H; rewrite H;
+  match goal with 
+  | [|- context [ ?xx ?< b ]] => 
+    generalize (is_lt_spec xx b);destruct (xx ?< b)
+  | _ => idtac
+  end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto.
+  rewrite PminusN_le...
+  generalize H1; zsimpl; auto.
+  rewrite PminusN_le...
+  generalize H1; zsimpl; auto.
+  intros p H; rewrite H; simpl; intros H1; split; auto.
+  zsimpl; ring.
+  intros p p1 H; rewrite H.
+  match goal with 
+  | [|- context [ ?xx ?< b ]] => 
+    generalize (is_lt_spec xx b);destruct (xx ?< b)
+  | _ => idtac
+  end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring.
+  rewrite PminusN_le...
+  generalize H1; zsimpl; auto.
+  rewrite PminusN_le...
+  generalize H1; zsimpl; auto.
+  match goal with 
+  | [|- context [ ?xx ?< b ]] => 
+    generalize (is_lt_spec xx b);destruct (xx ?< b)
+  | _ => idtac
+  end; zsimpl; simpl.
+  split; auto.
+  case (Zle_lt_or_eq 1 b); auto with zarith.
+  generalize (Zlt_0_pos b); auto with zarith.
+Qed.
+Transparent Zmult.
+
+(******** Definition du modulo ************)
+
+(* [mod a b] return [a] modulo [b] *)
+Fixpoint Pmod (a b : positive) {struct a} : N :=
+  match a with
+  | xH => if 1 ?< b then 1%N else 0%N
+  | xO a' =>
+    let r := Pmod a' b in
+    match r with
+    | N0 => 0%N
+    | Npos r' =>
+      if (xO r') ?< b then Npos (xO r')
+      else PminusN (xO r') b 
+    end
+  | xI a' =>
+    let r := Pmod a' b in
+    match r with
+    | N0 => if 1 ?< b then 1%N else 0%N
+    | Npos r' => 
+      if (xI r') ?< b then Npos (xI r')
+      else PminusN (xI r') b 
+    end
+  end.
+
+Infix "mod" := Pmod (at level 40, no associativity) : P_scope.
+Open Local Scope P_scope.
+
+Lemma Pmod_div_eucl : forall a b, a mod b = snd (a/b).
+Proof with auto.
+ intros a b;generalize a;clear a;induction a;simpl;
+ try (rewrite IHa;
+  assert (H1 := div_eucl_spec a b); destruct (a/b) as [q r];
+  destruct q as [|q];destruct r as [|r];simpl in *;
+  match goal with 
+   | [|- context [ ?xx ?< b ]] => 
+      assert (H2 := is_lt_spec xx b);destruct (xx ?< b)
+  | _ => idtac
+  end;simpl) ...
+ destruct H1 as [H3 H4];discriminate H3.
+ destruct (1 ?< b);simpl ...
+Qed.
+
+Lemma mod1: forall a, a mod 1 = 0%N.
+Proof. induction a;simpl;try rewrite IHa;trivial. Qed.
+
+Lemma mod_a_a_0 : forall a, a mod a = N0.
+Proof.
+ intros a;generalize (div_eucl_spec a a);rewrite <- Pmod_div_eucl.
+ destruct (fst (a / a));unfold Z_of_N at 1.
+ rewrite Zmult_0_l;intros (H1,H2);elimtype False;omega.
+ assert (a<=p*a).
+  pattern (Zpos a) at 1;rewrite <- (Zmult_1_l a).
+  assert (H1:= Zlt_0_pos p);assert (H2:= Zle_0_pos a);
+   apply Zmult_le_compat;trivial;try omega.
+ destruct (a mod a)%P;auto with zarith.
+ unfold Z_of_N;assert (H1:= Zlt_0_pos p0);intros (H2,H3);elimtype False;omega.
+Qed.
+  
+Lemma mod_le_2r : forall (a b r: positive) (q:N),
+                    Zpos a = b*q + r -> b <= a -> r < b -> 2*r <= a.
+Proof.
+ intros a b r q H0 H1 H2.
+ assert (H3:=Zlt_0_pos a). assert (H4:=Zlt_0_pos b). assert (H5:=Zlt_0_pos r). 
+ destruct q as [|q].  rewrite Zmult_0_r in H0. elimtype False;omega. 
+ assert (H6:=Zlt_0_pos q).  unfold Z_of_N in H0. 
+ assert (Zpos r = a - b*q). omega.
+ simpl;zsimpl. pattern r at 2;rewrite H.
+ assert (b <= b * q). 
+  pattern (Zpos b) at 1;rewrite <- (Zmult_1_r b).
+  apply Zmult_le_compat;try omega.
+ apply Zle_trans with (a - b * q + b). omega.
+ apply Zle_trans with (a - b + b);omega.
+Qed.
+
+Lemma mod_lt : forall a b r, a mod b = Npos r -> r < b.
+Proof.
+ intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl;
+  rewrite H;simpl;intros (H1,H2);omega.
+Qed.
+ 
+Lemma mod_le : forall a b r, a mod b = Npos r -> r <= b.
+Proof. intros a b r H;assert (H1:= mod_lt _ _ _ H);omega. Qed.
+
+Lemma mod_le_a : forall a b r, a mod b = r -> r <= a.
+Proof.
+ intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl;
+  rewrite H;simpl;intros (H1,H2).
+ assert (0 <= fst (a / b) * b). 
+  destruct (fst (a / b));simpl;auto with zarith.
+ auto with zarith.
+Qed.
+
+Lemma lt_mod : forall a b, Zpos a < Zpos b -> (a mod b)%P = Npos a.
+Proof.
+  intros a b H; rewrite Pmod_div_eucl. case (div_eucl_spec a b).
+  assert (0 <= snd(a/b)). destruct (snd(a/b));simpl;auto with zarith.
+  destruct (fst (a/b)).
+  unfold Z_of_N at 1;rewrite Zmult_0_l;rewrite Zplus_0_l.
+  destruct (snd (a/b));simpl; intros H1 H2;inversion H1;trivial.
+  unfold Z_of_N at 1;assert (b <= p*b).
+  pattern (Zpos b) at 1; rewrite <- (Zmult_1_l (Zpos b)).
+   assert (H1 := Zlt_0_pos p);apply Zmult_le_compat;try omega.
+  apply Zle_0_pos.
+  intros;elimtype False;omega.
+Qed.
+
+Fixpoint gcd_log2 (a b c:positive) {struct c}: option positive :=
+ match a mod b with
+ | N0  => Some b
+ | Npos r =>
+   match b mod r, c with
+   | N0, _ => Some r
+   | Npos r', xH    => None
+   | Npos r', xO c' => gcd_log2 r r' c'
+   | Npos r', xI c' => gcd_log2 r r' c'
+   end
+ end.
+
+Fixpoint egcd_log2 (a b c:positive) {struct c}: 
+    option (Z * Z * positive) :=
+ match a/b with
+ |    (_, N0)  => Some (0, 1, b)
+ | (q, Npos r) =>
+   match b/r, c with
+   | (_, N0), _ => Some (1, -q, r)
+   | (q', Npos r'), xH    => None
+   | (q', Npos r'), xO c' => 
+        match egcd_log2 r r' c' with
+          None => None
+        | Some (u', v', w') =>
+               let u := u' - v' * q' in
+               Some (u, v' - q * u, w')
+        end
+   | (q', Npos r'), xI c' => 
+        match egcd_log2 r r' c' with
+          None => None
+        | Some (u', v', w') =>
+               let u := u' - v' * q' in
+               Some (u, v' - q * u, w')
+        end
+   end
+ end.
+
+Lemma egcd_gcd_log2: forall c a b, 
+  match egcd_log2 a b c, gcd_log2 a b c with
+    None, None => True
+  | Some (u,v,r), Some r' => r = r'
+  | _, _ => False
+  end.
+induction c; simpl; auto; try 
+ (intros a b; generalize (Pmod_div_eucl a b); case (a/b); simpl;
+  intros q r1 H; subst; case (a mod b); auto;
+  intros r; generalize (Pmod_div_eucl b r); case (b/r); simpl;
+  intros q' r1 H; subst; case (b mod r); auto;
+  intros r'; generalize (IHc r r'); case egcd_log2; auto;
+  intros ((p1,p2),p3); case gcd_log2; auto).
+Qed.
+
+Ltac rw l := 
+  match l with
+   | (?r, ?r1) =>
+       match type of r with
+         True => rewrite <- r1
+      |  _ => rw r; rw r1
+      end 
+  | ?r => rewrite r
+  end. 
+
+Lemma egcd_log2_ok: forall c a b, 
+  match egcd_log2 a b c with
+    None => True
+  | Some (u,v,r) => u * a + v * b = r
+  end.
+induction c; simpl; auto;
+ intros a b; generalize (div_eucl_spec a b); case (a/b); 
+  simpl fst; simpl snd; intros q r1; case r1; try (intros; ring);
+  simpl; intros r (Hr1, Hr2); clear r1;
+  generalize (div_eucl_spec b r); case (b/r); 
+  simpl fst; simpl snd; intros q' r1; case r1; 
+    try (intros; rewrite Hr1; ring);
+  simpl; intros r' (Hr'1, Hr'2); clear r1; auto;
+  generalize (IHc r r'); case egcd_log2; auto;
+  intros ((u',v'),w'); case gcd_log2; auto; intros;
+  rw ((I, H), Hr1, Hr'1); ring.
+Qed.
+
+
+Fixpoint log2 (a:positive) : positive := 
+ match a with 
+ | xH => xH
+ | xO a => Psucc (log2 a) 
+ | xI a => Psucc (log2 a) 
+ end.
+
+Lemma gcd_log2_1: forall a c, gcd_log2  a xH c = Some xH.
+Proof. destruct c;simpl;try rewrite mod1;trivial. Qed.
+
+Lemma log2_Zle :forall a b, Zpos a <= Zpos b -> log2 a <= log2 b.
+Proof with zsimpl;try omega.
+ induction a;destruct b;zsimpl;intros;simpl ...
+ assert (log2 a <= log2 b) ...  apply IHa ...
+ assert (log2 a <= log2 b) ...  apply IHa ...
+ assert (H1 := Zlt_0_pos a);elimtype False;omega.
+ assert (log2 a <= log2 b) ...  apply IHa ...
+ assert (log2 a <= log2 b) ...  apply IHa ...
+ assert (H1 := Zlt_0_pos a);elimtype False;omega.
+ assert (H1 := Zlt_0_pos (log2 b)) ...
+ assert (H1 := Zlt_0_pos (log2 b)) ...
+Qed.
+
+Lemma log2_1_inv : forall a, Zpos (log2 a) = 1 -> a = xH.
+Proof.
+ destruct a;simpl;zsimpl;intros;trivial.
+ assert (H1:= Zlt_0_pos (log2 a));elimtype False;omega.
+ assert (H1:= Zlt_0_pos (log2 a));elimtype False;omega.
+Qed.
+
+Lemma mod_log2 : 
+  forall a b r:positive, a mod b = Npos r -> b <= a -> log2 r + 1 <= log2 a.
+Proof.
+ intros; cut (log2 (xO r) <= log2 a). simpl;zsimpl;trivial.
+ apply log2_Zle.
+ replace (Zpos (xO r)) with (2 * r)%Z;trivial. 
+ generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl;rewrite H.
+ rewrite Zmult_comm;intros [H1 H2];apply mod_le_2r with b (fst (a/b));trivial.
+Qed.
+
+Lemma gcd_log2_None_aux :
+  forall c a b, Zpos b <= Zpos a -> log2 b <= log2 c -> 
+   gcd_log2 a b c <> None.
+Proof.
+ induction c;simpl;intros;
+ (CaseEq (a mod b);[intros Heq|intros r Heq];try (intro;discriminate));
+ (CaseEq (b mod r);[intros Heq'|intros r' Heq'];try (intro;discriminate)).
+ apply IHc. apply mod_le with b;trivial.
+ generalize H0 (mod_log2 _ _ _ Heq' (mod_le _ _ _ Heq));zsimpl;intros;omega.
+ apply IHc. apply mod_le with b;trivial.
+ generalize H0 (mod_log2 _ _ _ Heq' (mod_le _ _ _ Heq));zsimpl;intros;omega.
+ assert (Zpos (log2 b) = 1).
+  assert (H1 := Zlt_0_pos (log2 b));omega.
+ rewrite (log2_1_inv _ H1) in Heq;rewrite mod1 in Heq;discriminate Heq.
+Qed.
+                    
+Lemma gcd_log2_None : forall a b, Zpos b <= Zpos a -> gcd_log2 a b b <> None.
+Proof. intros;apply gcd_log2_None_aux;auto with zarith. Qed.
+ 
+Lemma gcd_log2_Zle :
+   forall c1 c2 a b, log2 c1 <= log2 c2 -> 
+      gcd_log2 a b c1 <> None -> gcd_log2 a b c2 = gcd_log2 a b c1.
+Proof with zsimpl;trivial;try omega.
+ induction c1;destruct c2;simpl;intros;
+   (destruct (a mod b) as [|r];[idtac | destruct (b mod r)]) ...
+ apply IHc1;trivial. generalize H;zsimpl;intros;omega.
+ apply IHc1;trivial. generalize H;zsimpl;intros;omega.
+ elim H;destruct (log2 c1);trivial.
+ apply IHc1;trivial. generalize H;zsimpl;intros;omega.
+ apply IHc1;trivial. generalize H;zsimpl;intros;omega.
+ elim H;destruct (log2 c1);trivial.
+ elim H0;trivial. elim H0;trivial.
+Qed.
+
+Lemma gcd_log2_Zle_log :
+   forall a b c, log2 b <= log2 c -> Zpos b <= Zpos a ->
+      gcd_log2 a b c = gcd_log2 a b b.
+Proof.
+ intros a b c H1 H2; apply gcd_log2_Zle; trivial.
+ apply gcd_log2_None; trivial.
+Qed.
+ 
+Lemma gcd_log2_mod0 : 
+  forall a b c, a mod b = N0 -> gcd_log2 a b c = Some b.
+Proof. intros a b c H;destruct c;simpl;rewrite H;trivial. Qed.
+
+
+Require Import Zwf.
+
+Lemma Zwf_pos : well_founded (fun x y => Zpos x < Zpos y).
+Proof.
+ unfold well_founded.
+ assert (forall x a ,x = Zpos a -> Acc (fun x y : positive => x < y) a).
+ intros x;assert (Hacc := Zwf_well_founded 0 x);induction Hacc;intros;subst x.
+ constructor;intros. apply H0 with (Zpos y);trivial.
+ split;auto with zarith.
+ intros a;apply H with (Zpos a);trivial.
+Qed.
+
+Opaque Pmod.
+Lemma gcd_log2_mod : forall a b, Zpos b <= Zpos a -> 
+  forall r, a mod b = Npos r -> gcd_log2 a b b = gcd_log2 b r r.
+Proof.
+ intros a b;generalize a;clear a; assert (Hacc := Zwf_pos b).
+ induction Hacc; intros a Hle r Hmod.
+ rename x into b. destruct b;simpl;rewrite Hmod.
+ CaseEq (xI b mod r)%P;intros. rewrite gcd_log2_mod0;trivial.
+ assert (H2 := mod_le _ _ _ H1);assert (H3 := mod_lt _ _ _ Hmod);
+  assert (H4 := mod_le _ _ _ Hmod).
+ rewrite (gcd_log2_Zle_log r p b);trivial.
+ symmetry;apply H0;trivial.
+ generalize (mod_log2 _ _ _ H1 H4);simpl;zsimpl;intros;omega.
+ CaseEq (xO b mod r)%P;intros. rewrite gcd_log2_mod0;trivial.
+ assert (H2 := mod_le _ _ _ H1);assert (H3 := mod_lt _ _ _ Hmod);
+  assert (H4 := mod_le _ _ _ Hmod).
+ rewrite (gcd_log2_Zle_log r p b);trivial.
+ symmetry;apply H0;trivial.
+ generalize (mod_log2 _ _ _ H1 H4);simpl;zsimpl;intros;omega.
+ rewrite mod1 in Hmod;discriminate Hmod.
+Qed.
+
+Lemma gcd_log2_xO_Zle : 
+ forall a b, Zpos b <= Zpos a -> gcd_log2 a b (xO b) = gcd_log2 a b b.
+Proof.
+ intros a b Hle;apply gcd_log2_Zle.
+ simpl;zsimpl;auto with zarith.
+ apply gcd_log2_None_aux;auto with zarith.
+Qed.
+
+Lemma gcd_log2_xO_Zlt : 
+ forall a b, Zpos a < Zpos b -> gcd_log2 a b (xO b) = gcd_log2 b a a.
+Proof.
+ intros a b H;simpl. assert (Hlt := Zlt_0_pos a).
+ assert (H0 := lt_mod _ _ H).
+ rewrite H0;simpl.
+ CaseEq (b mod a)%P;intros;simpl.
+ symmetry;apply gcd_log2_mod0;trivial.
+ assert (H2 := mod_lt _ _ _ H1).
+ rewrite (gcd_log2_Zle_log a p b);auto with zarith.
+ symmetry;apply gcd_log2_mod;auto with zarith.
+ apply log2_Zle. 
+ replace (Zpos p) with (Z_of_N (Npos p));trivial.
+ apply mod_le_a with a;trivial.
+Qed.
+
+Lemma gcd_log2_x0 : forall a b, gcd_log2 a b (xO b) <> None.
+Proof.
+ intros;simpl;CaseEq (a mod b)%P;intros. intro;discriminate.
+ CaseEq (b mod p)%P;intros. intro;discriminate.
+ assert (H1 := mod_le_a _ _ _ H0). unfold Z_of_N in H1.
+ assert (H2 := mod_le _ _ _ H0).
+ apply gcd_log2_None_aux. trivial.
+ apply log2_Zle. trivial.
+Qed.
+
+Lemma egcd_log2_x0 : forall a b, egcd_log2 a b (xO b) <> None.
+Proof.
+intros a b H; generalize (egcd_gcd_log2 (xO b) a b) (gcd_log2_x0 a b);
+  rw H; case gcd_log2; auto.
+Qed.
+
+Definition gcd a b :=
+  match gcd_log2 a b (xO b) with
+  | Some p => p 
+  | None => (* can not appear *) 1%positive
+  end.
+
+Definition egcd a b :=
+  match egcd_log2 a b (xO b) with
+  | Some p => p 
+  | None => (* can not appear *) (1,1,1%positive)
+  end.
+
+
+Lemma gcd_mod0 : forall a b, (a mod b)%P = N0 -> gcd a b = b.
+Proof.
+ intros a b H;unfold gcd.
+ pattern (gcd_log2 a b (xO b)) at 1;
+  rewrite (gcd_log2_mod0 _ _ (xO b) H);trivial.
+Qed.
+
+Lemma gcd1 : forall a, gcd a xH = xH.
+Proof. intros a;rewrite gcd_mod0;[trivial|apply mod1]. Qed.
+
+Lemma gcd_mod : forall a b r, (a mod b)%P = Npos r ->
+                     gcd a b = gcd b r.
+Proof.
+ intros a b r H;unfold gcd.
+ assert (log2 r <= log2 (xO r)). simpl;zsimpl;omega.
+ assert (H1 := mod_lt _ _ _ H).
+ pattern (gcd_log2 b r (xO r)) at 1; rewrite gcd_log2_Zle_log;auto with zarith.
+ destruct (Z_lt_le_dec a b) as [z|z].
+ pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_xO_Zlt;trivial.
+ rewrite (lt_mod _ _ z) in H;inversion H.
+ assert  (r <= b). omega. 
+ generalize (gcd_log2_None _ _ H2).
+ destruct (gcd_log2 b r r);intros;trivial. 
+ assert (log2 b <= log2 (xO b)). simpl;zsimpl;omega.
+ pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_Zle_log;auto with zarith.
+ pattern (gcd_log2 a b b) at 1;rewrite (gcd_log2_mod _ _ z _ H).
+ assert  (r <= b). omega. 
+ generalize (gcd_log2_None _ _ H3).
+ destruct (gcd_log2 b r r);intros;trivial. 
+Qed.
+
+Require Import ZArith.
+Require Import Znumtheory.
+
+Hint Rewrite  Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc.
+
+Ltac mauto := 
+  trivial;autorewrite with zmisc;trivial;auto with zarith.
+
+Lemma gcd_Zis_gcd : forall a b:positive, (Zis_gcd b a (gcd b a)%P).
+Proof with mauto.
+ intros a;assert (Hacc := Zwf_pos a);induction Hacc;rename x into a;intros.
+ generalize (div_eucl_spec b a)...
+ rewrite <- (Pmod_div_eucl b a).
+ CaseEq (b mod a)%P;[intros Heq|intros r Heq]; intros (H1,H2).
+ simpl in H1;rewrite Zplus_0_r in H1.
+ rewrite (gcd_mod0 _ _ Heq).
+ constructor;mauto.
+ apply Zdivide_intro with (fst (b/a)%P);trivial.
+ rewrite (gcd_mod _ _ _ Heq).
+ rewrite H1;apply Zis_gcd_sym.
+ rewrite Zmult_comm;apply Zis_gcd_for_euclid2;simpl in *.
+ apply Zis_gcd_sym;auto.
+Qed.
+
+Lemma egcd_Zis_gcd : forall a b:positive, 
+   let (uv,w) := egcd a b in 
+   let  (u,v) := uv in 
+     u * a + v * b = w /\ (Zis_gcd b a w).
+Proof with mauto.
+ intros a b; unfold egcd.
+ generalize (egcd_log2_ok (xO b) a b) (egcd_gcd_log2 (xO b) a b) 
+            (egcd_log2_x0 a b) (gcd_Zis_gcd b a); unfold egcd, gcd.
+ case egcd_log2; try (intros ((u,v),w)); case gcd_log2;
+ try (intros; match goal with H: False |- _ => case H end);
+ try (intros _ _ H1; case H1; auto; fail).
+ intros; subst; split; try apply Zis_gcd_sym; auto.
+Qed.
+
+Definition Zgcd a b := 
+  match a, b with
+  | Z0, _ => b
+  | _, Z0 => a
+  | Zpos a, Zneg b => Zpos (gcd a b)
+  | Zneg a, Zpos b => Zpos (gcd a b)
+  | Zpos a, Zpos b => Zpos (gcd a b)
+  | Zneg a, Zneg b => Zpos (gcd a b)
+  end.
+
+
+Lemma Zgcd_is_gcd : forall x y, Zis_gcd x y (Zgcd x y).
+Proof.
+ destruct x;destruct y;simpl.
+ apply Zis_gcd_0.
+ apply Zis_gcd_sym;apply Zis_gcd_0. 
+ apply Zis_gcd_sym;apply Zis_gcd_0. 
+ apply Zis_gcd_0.
+ apply gcd_Zis_gcd.
+ apply Zis_gcd_sym;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd.
+ apply Zis_gcd_0.
+ apply Zis_gcd_minus;simpl;apply Zis_gcd_sym;apply gcd_Zis_gcd.
+ apply Zis_gcd_minus;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd.
+Qed.
+
+Definition Zegcd a b := 
+  match a, b with
+  | Z0, Z0 => (0,0,0)
+  | Zpos _, Z0 => (1,0,a)
+  | Zneg _, Z0 => (-1,0,-a)
+  | Z0, Zpos _ => (0,1,b)
+  | Z0, Zneg _ => (0,-1,-b)
+  | Zpos a, Zneg b => 
+     match egcd a b with (u,v,w) => (u,-v, Zpos w) end
+  | Zneg a, Zpos b =>
+     match egcd a b with (u,v,w) => (-u,v, Zpos w) end
+  | Zpos a, Zpos b => 
+     match egcd a b with (u,v,w) => (u,v, Zpos w) end
+  | Zneg a, Zneg b => 
+     match egcd a b with (u,v,w) => (-u,-v, Zpos w) end
+  end.
+
+Lemma Zegcd_is_egcd : forall x y, 
+  match Zegcd x y with
+   (u,v,w) => u * x + v * y = w /\ Zis_gcd x y w /\ 0 <= w
+  end.
+Proof.
+ assert (zx0: forall x, Zneg x = -x).
+    simpl; auto.
+ assert (zx1: forall x, -(-x) = x).
+   intro x; case x; simpl; auto.
+ destruct x;destruct y;simpl; try (split; [idtac|split]);
+  auto; try (red; simpl; intros; discriminate);
+ try (rewrite zx0; apply Zis_gcd_minus; try rewrite zx1; auto;
+       apply Zis_gcd_minus; try rewrite zx1; simpl; auto);
+ try apply Zis_gcd_0; try (apply Zis_gcd_sym;apply Zis_gcd_0);
+ generalize (egcd_Zis_gcd p p0); case egcd; intros (u,v) w (H1, H2); 
+ split; repeat rewrite zx0; try (rewrite <- H1; ring); auto;
+ (split; [idtac | red; intros; discriminate]).
+ apply Zis_gcd_sym; auto.
+ apply Zis_gcd_sym; apply Zis_gcd_minus; rw zx1; 
+    apply Zis_gcd_sym; auto.
+ apply Zis_gcd_minus; rw zx1; auto.
+ apply Zis_gcd_minus; rw zx1; auto.
+ apply Zis_gcd_minus; rw zx1; auto.
+ apply Zis_gcd_sym; auto.
+Qed.
diff --git a/coqprime/Z/ZCAux.v b/coqprime/Z/ZCAux.v
new file mode 100644
index 000000000..de03a2fe2
--- /dev/null
+++ b/coqprime/Z/ZCAux.v
@@ -0,0 +1,295 @@
+
+(*************************************************************)
+(*      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      *)
+(*************************************************************)
+
+(**********************************************************************
+     ZCAux.v                                                                                           
+                                                                                                          
+     Auxillary functions & Theorems                                              
+ **********************************************************************)
+
+Require Import ArithRing.
+Require Export ZArith Zpow_facts.
+Require Export Znumtheory.
+Require Export Tactic.
+
+Theorem Zdivide_div_prime_le_square:  forall x, 1 < x -> ~prime x -> exists p, prime p /\ (p | x) /\ p * p <= x.
+intros x Hx; generalize Hx; pattern x; apply Z_lt_induction; auto with zarith.
+clear x Hx; intros x Rec H H1.
+case (not_prime_divide x); auto.
+intros x1 ((H2, H3), H4); case (prime_dec x1); intros H5.
+case (Zle_or_lt (x1 * x1) x); intros H6.
+exists x1; auto.
+case H4; clear H4; intros x2 H4; subst.
+assert (Hx2: x2 <= x1).
+case (Zle_or_lt x2 x1); auto; intros H8; contradict H6; apply Zle_not_lt.
+apply Zmult_le_compat_r; auto with zarith.
+case (prime_dec x2); intros H7.
+exists x2; repeat (split; auto with zarith).
+apply Zmult_le_compat_l; auto with zarith.
+apply Zle_trans with 2%Z; try apply prime_ge_2; auto with zarith.
+case (Zle_or_lt 0 x2); intros H8.
+case Zle_lt_or_eq with (1 := H8); auto with zarith; clear H8; intros H8; subst; auto with zarith.
+case (Zle_lt_or_eq 1 x2); auto with zarith; clear H8; intros H8; subst; auto with zarith.
+case (Rec x2); try split; auto with zarith.
+intros x3 (H9, (H10, H11)).
+exists x3; repeat (split; auto with zarith).
+contradict H; apply Zle_not_lt; auto with zarith.
+apply Zle_trans with (0 * x1);  auto with zarith.
+case (Rec x1); try split; auto with zarith.
+intros x3 (H9, (H10, H11)).
+exists x3; repeat (split; auto with zarith).
+apply Zdivide_trans with x1; auto with zarith.
+Qed.
+
+
+Theorem Zmult_interval: forall p q, 0 < p * q  -> 1 < p -> 0 < q < p * q.
+intros p q H1 H2; assert (0 < q).
+case (Zle_or_lt q 0); auto; intros H3; contradict H1; apply Zle_not_lt.
+rewrite <- (Zmult_0_r p).
+apply Zmult_le_compat_l; auto with zarith.
+split; auto.
+pattern q at 1; rewrite <- (Zmult_1_l q).
+apply Zmult_lt_compat_r; auto with zarith.
+Qed.
+
+Theorem prime_induction: forall (P: Z -> Prop), P 0 -> P 1 -> (forall p q, prime p -> P q -> P (p * q)) -> forall p, 0 <= p -> P p. 
+intros P H H1 H2 p Hp.
+generalize Hp; pattern p; apply Z_lt_induction; auto; clear p Hp.
+intros p Rec Hp.
+case Zle_lt_or_eq with (1 := Hp); clear Hp; intros Hp; subst; auto.
+case (Zle_lt_or_eq  1 p); auto with zarith; clear Hp; intros Hp; subst; auto.
+case (prime_dec p); intros H3.
+rewrite <- (Zmult_1_r p); apply H2; auto.
+ case (Zdivide_div_prime_le_square p); auto.
+intros q (Hq1, ((q2, Hq2), Hq3)); subst.
+case (Zmult_interval q q2).
+rewrite Zmult_comm; apply Zlt_trans with 1; auto with zarith.
+apply Zlt_le_trans with 2; auto with zarith; apply prime_ge_2; auto.
+intros H4 H5; rewrite Zmult_comm; apply H2; auto.
+apply Rec; try split; auto with zarith.
+rewrite Zmult_comm; auto.
+Qed.
+
+Theorem div_power_max: forall p q, 1 < p -> 0 < q -> exists n, 0 <= n /\ (p ^n | q)  /\ ~(p ^(1 + n) | q).
+intros p q H1 H2; generalize H2; pattern q; apply Z_lt_induction; auto with zarith; clear q H2.
+intros q Rec H2.
+case (Zdivide_dec p q); intros H3.
+case (Zdivide_Zdiv_lt_pos p q); auto with zarith; intros H4 H5.
+case (Rec (Zdiv q p)); auto with zarith.
+intros n (Ha1, (Ha2, Ha3)); exists (n + 1); split; auto with zarith; split.
+case Ha2; intros q1 Hq; exists q1.
+rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
+rewrite  Zmult_assoc; rewrite <- Hq.
+rewrite Zmult_comm; apply Zdivide_Zdiv_eq; auto with zarith.
+intros (q1, Hu); case Ha3; exists q1.
+apply Zmult_reg_r with p; auto with zarith.
+rewrite (Zmult_comm (q / p)); rewrite <- Zdivide_Zdiv_eq; auto with zarith.
+apply trans_equal with (1 := Hu); repeat rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith.
+ring.
+exists 0; repeat split; try rewrite Zpower_1_r; try rewrite Zpower_exp_0; auto with zarith.
+Qed.
+
+Theorem prime_div_induction: 
+  forall (P: Z -> Prop) n,
+    0 < n ->
+    (P 1) ->
+    (forall p i, prime p -> 0 <= i -> (p^i | n) -> P (p^i)) ->  
+    (forall p q, rel_prime p q -> P p -> P q -> P (p * q)) -> 
+   forall m, 0 <= m -> (m | n) -> P m. 
+intros P n P1 Hn H H1 m Hm.
+generalize Hm; pattern m; apply Z_lt_induction; auto; clear m Hm.
+intros m Rec Hm H2.
+case (prime_dec m); intros Hm1.
+rewrite <- Zpower_1_r; apply H; auto with zarith.
+rewrite Zpower_1_r; auto.
+case Zle_lt_or_eq with (1 := Hm); clear Hm; intros Hm; subst.
+2: contradict P1; case H2; intros; subst; auto with zarith.
+case (Zle_lt_or_eq 1 m); auto with zarith; clear Hm; intros Hm; subst; auto.
+case Zdivide_div_prime_le_square with m; auto.
+intros p (Hp1, (Hp2, Hp3)).
+case (div_power_max p m); auto with zarith.
+generalize (prime_ge_2 p Hp1); auto with zarith.
+intros i (Hi, (Hi1, Hi2)).
+case Zle_lt_or_eq with (1 := Hi); clear Hi; intros Hi.
+assert (Hpi: 0 < p ^ i).
+apply Zpower_gt_0; auto with zarith.
+apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
+rewrite (Z_div_exact_2 m (p ^ i)); auto with zarith. 
+apply H1; auto with zarith.
+apply rel_prime_sym; apply rel_prime_Zpower_r; auto with zarith.
+apply rel_prime_sym.
+apply prime_rel_prime; auto.
+contradict Hi2.
+case Hi1; intros; subst.
+rewrite Z_div_mult in Hi2; auto with zarith.
+case Hi2; intros q0 Hq0; subst.
+exists q0; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
+apply H; auto with zarith.
+apply Zdivide_trans with (1 := Hi1); auto.
+apply Rec; auto with zarith.
+split; auto with zarith.
+apply Z_div_pos; auto with zarith.
+apply Z_div_lt; auto with zarith.
+apply Zle_ge; apply Zle_trans with p.
+apply prime_ge_2; auto.
+pattern p at 1; rewrite <- Zpower_1_r; apply Zpower_le_monotone; auto with zarith.
+apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
+apply Z_div_pos; auto with zarith.
+apply Zdivide_trans with (2 := H2); auto.
+exists (p ^ i); apply Z_div_exact_2; auto with zarith.
+apply Zdivide_mod; auto with zarith.
+apply Zdivide_mod; auto with zarith.
+case Hi2; rewrite <- Hi; rewrite Zplus_0_r; rewrite Zpower_1_r; auto.
+Qed.
+
+Theorem prime_div_Zpower_prime: forall n p q, 0 <= n -> prime p -> prime q -> (p | q ^ n) -> p = q.
+intros n p q Hp Hq; generalize p q Hq; pattern n; apply natlike_ind; auto; clear n p q Hp Hq.
+intros  p q Hp Hq; rewrite Zpower_0_r.
+intros (r, H); subst.
+case (Zmult_interval p r); auto; try rewrite Zmult_comm.
+rewrite <- H; auto with zarith.
+apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
+rewrite <- H; intros H1 H2; contradict H2; auto with zarith.
+intros n1 H Rec p q Hp Hq; try rewrite Zpower_Zsucc; auto with zarith; intros H1.
+case prime_mult with (2 := H1); auto.
+intros H2; apply prime_div_prime; auto.
+Qed.
+
+Definition Zmodd  a b :=
+match a with
+| Z0 => 0
+| Zpos a' =>
+    match b with
+    | Z0 => 0
+    | Zpos _ => Zmod_POS a' b
+    | Zneg b' =>
+        let r := Zmod_POS a' (Zpos b') in
+        match r  with Z0 =>  0 |  _  =>   b + r end
+    end
+| Zneg a' =>
+    match b with
+    | Z0 => 0
+    | Zpos _ =>
+        let r := Zmod_POS a' b in
+        match r with Z0 =>  0 | _  =>  b - r end
+    | Zneg b' => - (Zmod_POS a' (Zpos b'))
+    end
+end.
+
+Theorem Zmodd_correct: forall a b, Zmodd a b = Zmod a b.
+intros a b; unfold Zmod; case a; simpl; auto.
+intros p; case b; simpl; auto.
+intros p1; refine (Zmod_POS_correct _ _); auto.
+intros p1; rewrite Zmod_POS_correct; auto.
+case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto.
+intros p; case b; simpl; auto.
+intros p1; rewrite Zmod_POS_correct; auto.
+case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto.
+intros p1; rewrite Zmod_POS_correct; simpl; auto.
+case (Zdiv_eucl_POS p (Zpos p1)); auto.
+Qed.
+
+Theorem prime_divide_prime_eq:
+ forall p1 p2, prime p1 -> prime p2 -> Zdivide p1 p2 ->  p1 = p2.
+intros p1 p2 Hp1 Hp2 Hp3.
+assert (Ha: 1 < p1).
+inversion Hp1; auto.
+assert (Ha1: 1 < p2).
+inversion Hp2; auto.
+case (Zle_lt_or_eq p1 p2); auto with zarith.
+apply Zdivide_le; auto with zarith.
+intros Hp4.
+case (prime_div_prime p1 p2); auto with zarith.
+Qed.
+
+Theorem Zdivide_Zpower: forall n m, 0 < n -> (forall p i, prime p -> 0 < i -> (p^i | n) -> (p^i | m)) -> (n | m).
+intros n m Hn; generalize m Hn; pattern n; apply prime_induction; auto with zarith; clear n m Hn.
+intros m H1; contradict H1; auto with zarith.
+intros p q H Rec m H1 H2.
+assert (H3: (p | m)).
+rewrite <- (Zpower_1_r p); apply H2; auto with zarith; rewrite Zpower_1_r; apply Zdivide_factor_r.
+case (Zmult_interval p q); auto.
+apply Zlt_le_trans with 2; auto with zarith; apply prime_ge_2; auto.
+case H3; intros k Hk; subst.
+intros Hq Hq1.
+rewrite (Zmult_comm k); apply Zmult_divide_compat_l.
+apply Rec; auto.
+intros p1 i Hp1 Hp2 Hp3.
+case (Z_eq_dec p p1); intros Hpp1; subst.
+case (H2 p1 (Zsucc i)); auto with zarith.
+rewrite Zpower_Zsucc; try apply Zmult_divide_compat_l; auto with zarith.
+intros q2 Hq2; exists q2.
+apply Zmult_reg_r with p1.
+contradict H; subst; apply not_prime_0.
+rewrite Hq2; rewrite Zpower_Zsucc; try ring; auto with zarith.
+apply Gauss with p.
+rewrite Zmult_comm; apply H2; auto.
+apply Zdivide_trans with (1:= Hp3).
+apply Zdivide_factor_l.
+apply rel_prime_sym; apply rel_prime_Zpower_r; auto with zarith.
+apply prime_rel_prime; auto.
+contradict Hpp1; apply prime_divide_prime_eq; auto.
+Qed.
+
+Theorem prime_divide_Zpower_Zdiv: forall m a p i, 0 <= i -> prime p -> (m | a) -> ~(m | (a/p)) -> (p^i | a) -> (p^i | m).
+intros m a p i Hi Hp (k, Hk) H (l, Hl); subst.
+case (Zle_lt_or_eq 0 i); auto with arith; intros Hi1; subst.
+assert (Hp0: 0 < p).
+apply Zlt_le_trans with 2; auto with zarith; apply prime_ge_2; auto.
+case (Zdivide_dec p k); intros H1.
+case H1; intros k' H2; subst.
+case H; replace (k' * p * m) with ((k' * m) * p); try ring; rewrite Z_div_mult; auto with zarith.
+apply Gauss with k.
+exists l; rewrite Hl; ring.
+apply rel_prime_sym; apply rel_prime_Zpower_r; auto.
+apply rel_prime_sym; apply prime_rel_prime; auto.
+rewrite Zpower_0_r; apply Zone_divide.
+Qed.
+
+Theorem Zle_square_mult: forall a b, 0 <= a <= b -> a * a <= b * b.
+intros a b (H1, H2); apply Zle_trans with (a * b); auto with zarith.
+Qed.
+
+Theorem Zlt_square_mult_inv: forall a b, 0 <= a -> 0 <= b -> a * a < b * b -> a < b.
+intros a b H1 H2 H3; case (Zle_or_lt b a); auto; intros H4; apply Zmult_lt_reg_r with a; 
+   contradict H3; apply Zle_not_lt; apply Zle_square_mult; auto.
+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_small a n); try split; auto with zarith.
+Qed.
+
+
+Theorem Zpow_mod_pos_Zpower_pos_correct: forall a m n, 0 < n -> Zpow_mod_pos a m n = (Zpower_pos a m) mod n.
+intros a m; elim m; simpl; auto.
+intros p Rec n H1; rewrite xI_succ_xO; rewrite Pplus_one_succ_r; rewrite <- Pplus_diag; auto.
+repeat rewrite Zpower_pos_is_exp; auto.
+repeat rewrite Rec; auto.
+replace (Zpower_pos a 1) with a; auto.
+2: unfold Zpower_pos; simpl; auto with zarith.
+repeat rewrite (fun x => (Zmult_mod x a)); auto. 
+rewrite  (Zmult_mod  (Zpower_pos a p)); auto. 
+case (Zpower_pos a p mod n); auto.
+intros p Rec n H1; rewrite <- Pplus_diag; auto.
+repeat rewrite Zpower_pos_is_exp; auto.
+repeat rewrite Rec; auto.
+rewrite  (Zmult_mod  (Zpower_pos a p)); auto. 
+case (Zpower_pos a p mod n); auto.
+unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith.
+Qed.
+
+Theorem Zpow_mod_Zpower_correct: forall a m n, 1 < n -> 0 <= m -> Zpow_mod a m n = (a ^ m) mod n.
+intros a m n; case m; simpl; auto.
+intros; apply Zpow_mod_pos_Zpower_pos_correct; auto with zarith.
+Qed.
diff --git a/coqprime/Z/ZCmisc.v b/coqprime/Z/ZCmisc.v
new file mode 100644
index 000000000..c1bdacc63
--- /dev/null
+++ b/coqprime/Z/ZCmisc.v
@@ -0,0 +1,186 @@
+
+(*************************************************************)
+(*      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      *)
+(*************************************************************)
+
+Require Export ZArith.
+Open Local Scope Z_scope.
+
+Coercion Zpos : positive >-> Z.
+Coercion Z_of_N : N >-> Z.
+
+Lemma Zpos_plus : forall p q, Zpos (p + q) = p + q.
+Proof. intros;trivial. Qed.
+
+Lemma Zpos_mult : forall p q, Zpos (p * q) = p * q.
+Proof. intros;trivial. Qed.
+
+Lemma Zpos_xI_add : forall p, Zpos (xI p) = Zpos p + Zpos p + Zpos 1.
+Proof. intros p;rewrite Zpos_xI;ring. Qed.
+
+Lemma Zpos_xO_add : forall p, Zpos (xO p) = Zpos p + Zpos p.
+Proof. intros p;rewrite Zpos_xO;ring. Qed.
+
+Lemma Psucc_Zplus : forall p, Zpos (Psucc p) = p + 1.
+Proof. intros p;rewrite Zpos_succ_morphism;unfold Zsucc;trivial. Qed.
+
+Hint Rewrite Zpos_xI_add Zpos_xO_add Pplus_carry_spec 
+ Psucc_Zplus Zpos_plus : zmisc.
+
+Lemma Zlt_0_pos : forall p, 0 < Zpos p.
+Proof. unfold Zlt;trivial. Qed.
+  
+
+Lemma Pminus_mask_carry_spec : forall p q, 
+  Pminus_mask_carry p q = Pminus_mask p (Psucc q).
+Proof.
+ intros p q;generalize q p;clear q p.
+ induction q;destruct p;simpl;try rewrite IHq;trivial.
+ destruct p;trivial.  destruct p;trivial.
+Qed.
+
+Hint Rewrite Pminus_mask_carry_spec : zmisc.
+
+Ltac zsimpl := autorewrite with zmisc.
+Ltac CaseEq t := generalize (refl_equal t);pattern t at -1;case t.
+Ltac generalizeclear H := generalize H;clear H.
+
+Lemma Pminus_mask_spec : 
+   forall p q, 
+    match Pminus_mask p q with
+    | IsNul    => Zpos p =  Zpos q
+    | IsPos k => Zpos p = q + k 
+    | IsNeq   => p < q
+    end.
+Proof with zsimpl;auto with zarith.
+ induction p;destruct q;simpl;zsimpl;
+  match goal with 
+  | [|- context [(Pminus_mask ?p1 ?q1)]] => 
+    assert (H1 := IHp q1);destruct (Pminus_mask p1 q1)
+  | _ => idtac
+  end;simpl ...
+ inversion H1 ...   inversion H1 ...
+ rewrite Psucc_Zplus in H1 ...
+ clear IHp;induction p;simpl ...
+  rewrite IHp;destruct (Pdouble_minus_one p) ...
+ assert (H:= Zlt_0_pos q) ...   assert (H:= Zlt_0_pos q) ...
+Qed.
+
+Definition PminusN x y := 
+  match Pminus_mask x y with
+  | IsPos k => Npos k
+  | _ => N0
+  end.
+
+Lemma PminusN_le : forall x y:positive, x <= y -> Z_of_N (PminusN y x) = y - x.
+Proof.
+ intros x y Hle;unfold PminusN.
+ assert (H := Pminus_mask_spec y x);destruct (Pminus_mask y x).
+ rewrite H;unfold Z_of_N;auto with zarith.
+ rewrite H;unfold Z_of_N;auto with zarith.
+ elimtype False;omega.
+Qed.
+
+Lemma Ppred_Zminus : forall p, 1< Zpos p ->  (p-1)%Z = Ppred p.
+Proof. destruct p;simpl;trivial. intros;elimtype False;omega. Qed.
+
+
+Open Local Scope positive_scope.
+
+Delimit Scope P_scope with P.
+Open Local Scope P_scope.
+
+Definition is_lt (n m : positive) :=
+  match (n ?= m) with
+  | Lt => true
+  | _ => false
+  end.
+Infix "?<" := is_lt (at level 70, no associativity) : P_scope.
+
+Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z. 
+Proof.
+intros n m; unfold is_lt, Zlt, Zle, Zcompare.
+rewrite Pos.compare_antisym.
+case (m ?= n); simpl; auto; intros HH; discriminate HH.
+Qed.
+
+Definition is_eq a b :=
+  match (a ?= b) with
+  | Eq => true
+  | _ => false
+  end.
+Infix "?=" := is_eq (at level 70, no associativity) : P_scope.
+ 
+Lemma is_eq_refl : forall n, n ?= n = true.
+Proof. intros n;unfold is_eq;rewrite Pos.compare_refl;trivial. Qed.
+
+Lemma is_eq_eq : forall n m, n ?= m = true -> n = m.
+Proof.
+ unfold is_eq;intros n m H; apply Pos.compare_eq.
+destruct (n ?= m)%positive;trivial;try discriminate.
+Qed.
+
+Lemma is_eq_spec_pos : forall n m, if n ?= m then  n = m else  m <> n. 
+Proof.
+ intros n m; CaseEq (n ?= m);intro H.
+ rewrite (is_eq_eq _ _ H);trivial.
+ intro H1;rewrite H1 in H;rewrite is_eq_refl in H;discriminate H.
+Qed.
+
+Lemma is_eq_spec : forall n m, if n ?= m then Zpos n = m else Zpos m <> n. 
+Proof.
+ intros n m; CaseEq (n ?= m);intro H.
+ rewrite (is_eq_eq _ _ H);trivial.
+ intro H1;inversion H1.
+ rewrite H2 in H;rewrite is_eq_refl in H;discriminate H.
+Qed.
+
+Definition is_Eq a b :=
+  match a, b with
+  | N0, N0 => true
+  | Npos a', Npos b' => a' ?= b'
+  | _, _ => false
+  end.
+
+Lemma is_Eq_spec : 
+ forall n m, if is_Eq n m then Z_of_N n = m else Z_of_N m <> n. 
+Proof.
+ destruct n;destruct m;simpl;trivial;try (intro;discriminate).
+ apply is_eq_spec.
+Qed.
+
+(* [times x y] return [x * y], a litle bit more efficiant *)
+Fixpoint times (x y : positive) {struct y} : positive :=
+  match x, y with
+  | xH, _ => y
+  | _, xH => x
+  | xO x', xO y' => xO (xO (times x' y'))
+  | xO x', xI y' => xO (x' + xO (times x' y'))
+  | xI x', xO y' => xO (y' + xO (times x' y'))
+  | xI x', xI y' => xI (x' + y' + xO (times x' y'))
+  end.
+
+Infix "*" := times : P_scope.
+
+Lemma times_Zmult : forall p q, Zpos (p * q)%P = (p * q)%Z.
+Proof.
+ intros p q;generalize q p;clear p q.
+ induction q;destruct p; unfold times; try fold (times p q);
+   autorewrite with zmisc; try rewrite IHq; ring.
+Qed.
+
+Fixpoint square (x:positive) : positive :=
+ match x with
+ | xH => xH
+ | xO x => xO (xO (square x))
+ | xI x => xI (xO (square x + x))
+ end.
+
+Lemma square_Zmult : forall x, Zpos (square x) = (x * x) %Z.
+Proof.
+ induction x as [x IHx|x IHx |];unfold square;try (fold (square x));
+   autorewrite with zmisc; try rewrite IHx; ring.
+Qed.
diff --git a/coqprime/Z/ZSum.v b/coqprime/Z/ZSum.v
new file mode 100644
index 000000000..3a7f14065
--- /dev/null
+++ b/coqprime/Z/ZSum.v
@@ -0,0 +1,335 @@
+
+(*************************************************************)
+(*      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      *)
+(*************************************************************)
+
+(***********************************************************************
+    Summation.v from Z to Z
+ *********************************************************************)
+Require Import Arith.
+Require Import ArithRing.
+Require Import ListAux.
+Require Import ZArith.
+Require Import Iterator.
+Require Import ZProgression.
+
+
+Open Scope Z_scope.
+(* Iterated Sum *)
+ 
+Definition Zsum :=
+   fun n m f =>
+   if Zle_bool n m
+     then iter 0 f Zplus (progression Zsucc n (Zabs_nat ((1 + m) - n)))
+     else iter 0 f Zplus (progression Zpred n (Zabs_nat ((1 + n) - m))).
+Hint Unfold Zsum .
+ 
+Lemma Zsum_nn: forall n f,  Zsum n n f = f n.
+intros n f; unfold Zsum; rewrite Zle_bool_refl.
+replace ((1 + n) - n) with 1; auto with zarith.
+simpl; ring.
+Qed.
+
+Theorem permutation_rev: forall (A:Set) (l : list A),  permutation (rev l) l.
+intros a l; elim l; simpl; auto.
+intros a1 l1 Hl1.
+apply permutation_trans with (cons a1 (rev l1)); auto.
+change (permutation (rev l1 ++ (a1 :: nil)) (app (cons a1 nil) (rev l1))); auto.
+Qed.
+ 
+Lemma Zsum_swap: forall (n m : Z) (f : Z ->  Z),  Zsum n m f = Zsum m n f.
+intros n m f; unfold Zsum.
+generalize (Zle_cases n m) (Zle_cases m n); case (Zle_bool n m);
+ case (Zle_bool m n); auto with arith.
+intros; replace n with m; auto with zarith.
+3:intros H1 H2; contradict H2; auto with zarith.
+intros H1 H2; apply iter_permutation; auto with zarith.
+apply permutation_trans
+     with (rev (progression Zsucc n (Zabs_nat ((1 + m) - n)))).
+apply permutation_sym; apply permutation_rev.
+rewrite Zprogression_opp; auto with zarith.
+replace (n + Z_of_nat (pred (Zabs_nat ((1 + m) - n)))) with m; auto.
+replace (Zabs_nat ((1 + m) - n)) with (S (Zabs_nat (m - n))); auto with zarith.
+simpl.
+rewrite inj_Zabs_nat; auto with zarith.
+rewrite Zabs_eq; auto with zarith.
+replace ((1 + m) - n) with (1 + (m - n)); auto with zarith.
+cut (0 <= m - n); auto with zarith; unfold Zabs_nat.
+case (m - n); auto with zarith.
+intros p; case p; simpl; auto with zarith.
+intros p1 Hp1; rewrite nat_of_P_xO; rewrite nat_of_P_xI;
+ rewrite nat_of_P_succ_morphism.
+simpl; repeat rewrite plus_0_r.
+repeat rewrite <- plus_n_Sm; simpl; auto.
+intros p H3; contradict H3; auto with zarith.
+intros H1 H2; apply iter_permutation; auto with zarith.
+apply permutation_trans
+     with (rev (progression Zsucc m (Zabs_nat ((1 + n) - m)))).
+rewrite Zprogression_opp; auto with zarith.
+replace (m + Z_of_nat (pred (Zabs_nat ((1 + n) - m)))) with n; auto.
+replace (Zabs_nat ((1 + n) - m)) with (S (Zabs_nat (n - m))); auto with zarith.
+simpl.
+rewrite inj_Zabs_nat; auto with zarith.
+rewrite Zabs_eq; auto with zarith.
+replace ((1 + n) - m) with (1 + (n - m)); auto with zarith.
+cut (0 <= n - m); auto with zarith; unfold Zabs_nat.
+case (n - m); auto with zarith.
+intros p; case p; simpl; auto with zarith.
+intros p1 Hp1; rewrite nat_of_P_xO; rewrite nat_of_P_xI;
+ rewrite nat_of_P_succ_morphism.
+simpl; repeat rewrite plus_0_r.
+repeat rewrite <- plus_n_Sm; simpl; auto.
+intros p H3; contradict H3; auto with zarith.
+apply permutation_rev.
+Qed.
+ 
+Lemma Zsum_split_up:
+ forall (n m p : Z) (f : Z ->  Z),
+ ( n <= m < p ) ->  Zsum n p f = Zsum n m f + Zsum (m + 1) p f.
+intros n m p f [H H0].
+case (Zle_lt_or_eq _ _ H); clear H; intros H.
+unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith.
+assert (H1: n < p).
+apply Zlt_trans with ( 1 := H ); auto with zarith.
+assert (H2: m < 1 + p).
+apply Zlt_trans with ( 1 := H0 ); auto with zarith.
+assert (H3: n < 1 + m).
+apply Zlt_trans with ( 1 := H ); auto with zarith.
+assert (H4: n < 1 + p).
+apply Zlt_trans with ( 1 := H1 ); auto with zarith.
+replace (Zabs_nat ((1 + p) - (m + 1)))
+     with (minus (Zabs_nat ((1 + p) - n)) (Zabs_nat ((1 + m) - n))).
+apply iter_progression_app; auto with zarith.
+apply inj_le_rev.
+(repeat rewrite inj_Zabs_nat); auto with zarith.
+(repeat rewrite Zabs_eq); auto with zarith.
+rewrite next_n_Z; auto with zarith.
+rewrite inj_Zabs_nat; auto with zarith.
+rewrite Zabs_eq; auto with zarith.
+apply inj_eq_rev; auto with zarith.
+rewrite inj_minus1; auto with zarith.
+(repeat rewrite inj_Zabs_nat); auto with zarith.
+(repeat rewrite Zabs_eq); auto with zarith.
+apply inj_le_rev.
+(repeat rewrite inj_Zabs_nat); auto with zarith.
+(repeat rewrite Zabs_eq); auto with zarith.
+subst m.
+rewrite Zsum_nn; auto with zarith.
+unfold Zsum; generalize (Zle_cases n p); generalize (Zle_cases (n + 1) p);
+ case (Zle_bool n p); case (Zle_bool (n + 1) p); auto with zarith.
+intros H1 H2.
+replace (Zabs_nat ((1 + p) - n)) with (S (Zabs_nat (p - n))); auto with zarith.
+replace (n + 1) with (Zsucc n); auto with zarith.
+replace ((1 + p) - Zsucc n) with (p - n); auto with zarith.
+apply inj_eq_rev; auto with zarith.
+rewrite inj_S; (repeat rewrite inj_Zabs_nat); auto with zarith.
+(repeat rewrite Zabs_eq); auto with zarith.
+Qed.
+ 
+Lemma Zsum_S_left:
+ forall (n m : Z) (f : Z ->  Z), n < m ->  Zsum n m f = f n + Zsum (n + 1) m f.
+intros n m f H; rewrite (Zsum_split_up n n m f); auto with zarith.
+rewrite Zsum_nn; auto with zarith.
+Qed.
+ 
+Lemma Zsum_S_right:
+ forall (n m : Z) (f : Z ->  Z),
+ n <= m ->  Zsum n (m + 1) f = Zsum n m f  + f (m + 1).
+intros n m f H; rewrite (Zsum_split_up n m (m + 1) f); auto with zarith.
+rewrite Zsum_nn; auto with zarith.
+Qed.
+  
+Lemma Zsum_split_down:
+ forall (n m p : Z) (f : Z ->  Z),
+ ( p < m <= n ) ->  Zsum n p f = Zsum n m f  + Zsum (m - 1) p f.
+intros n m p f [H H0].
+case (Zle_lt_or_eq p (m - 1)); auto with zarith; intros H1.
+pattern m at 1; replace m with ((m - 1) + 1); auto with zarith.
+repeat rewrite (Zsum_swap n).
+rewrite (Zsum_swap (m - 1)).
+rewrite Zplus_comm.
+apply Zsum_split_up; auto with zarith.
+subst p.
+repeat rewrite (Zsum_swap n).
+rewrite Zsum_nn.
+unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith.
+replace (Zabs_nat ((1 + n) - (m - 1))) with (S (Zabs_nat (n - (m - 1)))).
+rewrite Zplus_comm.
+replace (Zabs_nat ((1 + n) - m)) with (Zabs_nat (n - (m - 1))); auto with zarith.
+pattern m at 4; replace m with (Zsucc (m - 1)); auto with zarith.
+apply f_equal with ( f := Zabs_nat ); auto with zarith.
+apply inj_eq_rev; auto with zarith.
+rewrite inj_S.
+(repeat rewrite inj_Zabs_nat); auto with zarith.
+(repeat rewrite Zabs_eq); auto with zarith.
+Qed.
+
+
+Lemma Zsum_ext:
+ forall (n m : Z) (f g : Z ->  Z),
+ n <= m ->
+ (forall (x : Z), ( n <= x <= m ) ->  f x = g x) ->  Zsum n m f = Zsum n m g.
+intros n m f g HH H.
+unfold Zsum; auto.
+unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith.
+apply iter_ext; auto with zarith.
+intros a H1; apply H; auto; split.
+apply Zprogression_le_init with ( 1 := H1 ).
+cut (a < Zsucc m); auto with zarith.
+replace (Zsucc m) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith.
+apply Zprogression_le_end; auto with zarith.
+rewrite inj_Zabs_nat; auto with zarith.
+(repeat rewrite Zabs_eq); auto with zarith.
+Qed.
+
+Lemma Zsum_add:
+ forall (n m : Z) (f g : Z ->  Z),
+  Zsum n m f  + Zsum n m g = Zsum n m (fun (i : Z) => f i + g i).
+intros n m f g; unfold Zsum; case (Zle_bool n m); apply iter_comp;
+ auto with zarith.
+Qed.
+ 
+Lemma Zsum_times:
+ forall n m x f,  x * Zsum n m f = Zsum n m (fun i=> x * f i).
+intros n m x f.
+unfold Zsum. case (Zle_bool n m); intros; apply iter_comp_const with (k := (fun y : Z => x * y)); auto with zarith.
+Qed.
+ 
+Lemma inv_Zsum:
+ forall (P : Z ->  Prop) (n m : Z) (f : Z ->  Z),
+ n <= m ->
+ P 0 ->
+ (forall (a b : Z), P a -> P b ->  P (a + b)) ->
+ (forall (x : Z), ( n <= x <= m ) ->  P (f x)) ->  P (Zsum n m f).
+intros P n m f HH H H0 H1.
+unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith; apply iter_inv; auto.
+intros x H3; apply H1; auto; split.
+apply Zprogression_le_init with ( 1 := H3 ).
+cut (x < Zsucc m); auto with zarith.
+replace (Zsucc m) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith.
+apply Zprogression_le_end; auto with zarith.
+rewrite inj_Zabs_nat; auto with zarith.
+(repeat rewrite Zabs_eq); auto with zarith.
+Qed.
+
+
+Lemma Zsum_pred:
+ forall (n m : Z) (f : Z ->  Z),
+  Zsum n m f = Zsum (n + 1) (m + 1) (fun (i : Z) => f (Zpred i)).
+intros n m f.
+unfold Zsum.
+generalize (Zle_cases n m); generalize (Zle_cases (n + 1) (m + 1));
+ case (Zle_bool n m); case (Zle_bool (n + 1) (m + 1)); auto with zarith.
+replace ((1 + (m + 1)) - (n + 1)) with ((1 + m) - n); auto with zarith.
+intros H1 H2; cut (exists c , c = Zabs_nat ((1 + m) - n) ).
+intros [c H3]; rewrite <- H3.
+generalize n; elim c; auto with zarith; clear H1 H2 H3 c n.
+intros c H n; simpl; eq_tac; auto with zarith.
+eq_tac; unfold Zpred; auto with zarith.
+replace (Zsucc (n + 1)) with (Zsucc n + 1); auto with zarith.
+exists (Zabs_nat ((1 + m) - n)); auto.
+replace ((1 + (n + 1)) - (m + 1)) with ((1 + n) - m); auto with zarith.
+intros H1 H2; cut (exists c , c = Zabs_nat ((1 + n) - m) ).
+intros [c H3]; rewrite <- H3.
+generalize n; elim c; auto with zarith; clear H1 H2 H3 c n.
+intros c H n; simpl; (eq_tac; auto with zarith).
+eq_tac; unfold Zpred; auto with zarith.
+replace (Zpred (n + 1)) with (Zpred n + 1); auto with zarith.
+unfold Zpred; auto with zarith.
+exists (Zabs_nat ((1 + n) - m)); auto.
+Qed.
+ 
+Theorem Zsum_c:
+ forall (c p q : Z), p <= q ->  Zsum p q (fun x => c) = ((1 + q) - p) * c.
+intros c p q Hq; unfold Zsum.
+rewrite Zle_imp_le_bool; auto with zarith.
+pattern ((1 + q) - p) at 2.
+ rewrite <- Zabs_eq; auto with zarith.
+ rewrite <- inj_Zabs_nat; auto with zarith.
+cut (exists r , r = Zabs_nat ((1 + q) - p) );
+ [intros [r H1]; rewrite <- H1 | exists (Zabs_nat ((1 + q) - p))]; auto.
+generalize p; elim r; auto with zarith.
+intros n H p0; replace (Z_of_nat (S n)) with (Z_of_nat n + 1); auto with zarith.
+simpl; rewrite H; ring.
+rewrite inj_S; auto with zarith.
+Qed.
+ 
+Theorem Zsum_Zsum_f:
+ forall (i j k l : Z) (f : Z -> Z ->  Z),
+ i <= j ->
+ k < l ->
+  Zsum i j (fun x => Zsum k (l + 1) (fun y => f x y)) =
+  Zsum i j (fun x => Zsum k l (fun y => f x y) + f x (l + 1)).
+intros; apply Zsum_ext; intros; auto with zarith.
+rewrite Zsum_S_right; auto with zarith.
+Qed.
+ 
+Theorem Zsum_com:
+ forall (i j k l : Z) (f : Z -> Z ->  Z),
+  Zsum i j (fun x => Zsum k l (fun y => f x y)) =
+  Zsum k l (fun y => Zsum i j (fun x => f x y)).
+intros; unfold Zsum; case (Zle_bool i j); case (Zle_bool k l); apply iter_com;
+ auto with zarith.
+Qed.
+ 
+Theorem Zsum_le:
+ forall (n m : Z) (f g : Z ->  Z),
+ n <= m ->
+ (forall (x : Z), ( n <= x <= m ) ->  (f x <= g x )) ->
+  (Zsum n m f <= Zsum n m g ).
+intros n m f g Hl H.
+unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith.
+unfold Zsum;
+ cut
+  (forall x,
+   In x (progression Zsucc n (Zabs_nat ((1 + m) - n))) ->  ( f x <= g x )).
+elim (progression Zsucc n (Zabs_nat ((1 + m) - n))); simpl; auto with zarith.
+intros x H1; apply H; split.
+apply Zprogression_le_init with ( 1 := H1 ); auto.
+cut (x < m + 1); auto with zarith.
+replace (m + 1) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith.
+apply Zprogression_le_end; auto with zarith.
+rewrite inj_Zabs_nat; auto with zarith.
+rewrite Zabs_eq; auto with zarith.
+Qed.
+
+Theorem iter_le:
+forall (f g: Z -> Z)  l, (forall a, In a l -> f a <= g a) ->
+  iter 0 f Zplus l <= iter 0 g Zplus l.
+intros f g l; elim l; simpl; auto with zarith.
+Qed.
+ 
+Theorem Zsum_lt:
+ forall n m f g,
+ (forall x, n <= x -> x <= m ->  f x <= g x) ->
+ (exists x, n <= x /\ x <= m /\  f x < g x) ->
+  Zsum n m f < Zsum n m g.
+intros n m f g H (d, (Hd1, (Hd2, Hd3))); unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith.
+cut (In d (progression  Zsucc n (Zabs_nat (1 + m - n)))).
+cut (forall x, In x (progression Zsucc n (Zabs_nat (1 + m - n)))->  f x <= g x).
+elim (progression  Zsucc n (Zabs_nat (1 + m - n))); simpl; auto with zarith.
+intros a l Rec  H0 [H1 | H1]; subst; auto.
+apply Zle_lt_trans with (f d + iter 0 g Zplus l); auto with zarith.
+apply Zplus_le_compat_l.
+apply iter_le; auto.
+apply Zlt_le_trans with (f a + iter 0 g Zplus l); auto with zarith.
+intros x H1; apply H.
+apply Zprogression_le_init with ( 1 := H1 ); auto.
+cut (x < m + 1); auto with zarith.
+replace (m + 1) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith.
+apply Zprogression_le_end with ( 1 := H1 ); auto with arith.
+rewrite inj_Zabs_nat; auto with zarith.
+rewrite Zabs_eq; auto with zarith.
+apply in_Zprogression.
+rewrite inj_Zabs_nat; auto with zarith.
+rewrite Zabs_eq; auto with zarith.
+Qed.
+ 
+Theorem Zsum_minus:
+ forall n m f g,  Zsum n m f - Zsum n m g = Zsum n m (fun x => f x - g x).
+intros n m f g; apply trans_equal with (Zsum n m f + (-1) * Zsum n m g); auto with zarith.
+rewrite Zsum_times; rewrite Zsum_add; auto with zarith.
+Qed.