Strip trailing whitespace

With
```bash
bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh
```

24 files changed, 568 insertions, 571 deletions

diff --git a/coqprime/Coqprime/Cyclic.v b/coqprime/Coqprime/Cyclic.v
index c25f683ca..7a9d8e19b 100644
--- a/coqprime/Coqprime/Cyclic.v
+++ b/coqprime/Coqprime/Cyclic.v
@@ -7,9 +7,9 @@
 (*************************************************************)
 
 (***********************************************************************
-      Cyclic.v                                                                                       
-                                                                                                         
-      Proof that an abelien ring is cyclic                                 
+      Cyclic.v
+
+      Proof that an abelien ring is cyclic
  ************************************************************************)
 Require Import ZCAux.
 Require Import List.
@@ -50,13 +50,13 @@ Hypothesis op_internal: forall a, In a support -> In (op a) support.
 Hypothesis plus_op_zero: forall a, In a support -> plus a (op a) = zero.
 Hypothesis mult_integral: forall a b, In a support -> In b support -> mult a b = zero -> a = zero \/ b = zero.
 
-Definition IA := (IGroup A mult support e A_dec support_ulist e_in_support mult_internal 
+Definition IA := (IGroup A mult support e A_dec support_ulist e_in_support mult_internal
                              mult_assoc
                              e_is_zero_l e_is_zero_r).
 
 Hint Resolve (fun x => isupport_incl _ mult support e A_dec x).
 
-Theorem gpow_evaln: forall n, 0 < n -> 
+Theorem gpow_evaln: forall n, 0 < n ->
   exists p, (length p <=  Zabs_nat n)%nat /\  (forall i, In i p -> In i support) /\
   forall x, In x IA.(s) -> eval A plus mult zero (zero::p) x = gpow x IA n.
 intros n Hn; generalize Hn; pattern n; apply natlike_ind; auto with zarith.
@@ -92,7 +92,7 @@ intros l n; elim l; simpl; auto.
 intros H; left; intros a H1; case H1.
 intros a l1 Rec H.
 case (A_dec (gpow a IA n) e); intros H2.
-case Rec; try intros H3. 
+case Rec; try intros H3.
 apply incl_tran with (2 := H); auto with datatypes.
 left; intros a1 H4; case H4; auto.
 intros H5; rewrite <- H5; auto.
@@ -146,7 +146,7 @@ case (check_list_gpow IA.(s) i); try intros H; auto with datatypes.
 case (gpow_evaln i); auto; intros p (Hp1, (Hp2, Hp3)).
 absurd ((op e) = zero).
 intros H1; case e_not_zero.
-rewrite <- (plus_op_zero e); try rewrite H1; auto. 
+rewrite <- (plus_op_zero e); try rewrite H1; auto.
 rewrite plus_comm; auto.
 apply (root_max_is_zero _ (fun x => In x support) plus mult op zero) with (l := IA.(s)) (p := op e :: p); auto with datatypes.
 simpl; intros x [Hx | Hx]; try rewrite <- Hx; auto.
@@ -161,7 +161,7 @@ apply inj_lt_inv.
 rewrite inj_Zabs_nat; auto with zarith.
 rewrite Zabs_eq; auto with zarith.
 Qed.
- 
+
 Theorem divide_g_order_e_order: forall n, 0 <= n -> (n | g_order IA) -> exists a, In a IA.(s) /\ e_order A_dec  a IA = n.
 intros n Hn H.
 assert (Hg: 0 < g_order IA).
diff --git a/coqprime/Coqprime/EGroup.v b/coqprime/Coqprime/EGroup.v
index 933176abd..2752bb002 100644
--- a/coqprime/Coqprime/EGroup.v
+++ b/coqprime/Coqprime/EGroup.v
@@ -7,8 +7,8 @@
 (*************************************************************)
 
 (**********************************************************************
-    EGroup.v                                
-                                                                     
+    EGroup.v
+
     Given an element a, create the group {e, a, a^2, ..., a^n}
  **********************************************************************)
 Require Import ZArith.
@@ -38,10 +38,10 @@ Variable G: FGroup op.
 Hypothesis a_in_G: In a G.(s).
 
 
-(************************************** 
+(**************************************
   The power function for the group
  **************************************)
- 
+
 Set Implicit Arguments.
 Definition gpow n := match n with  Zpos p => iter_pos _ (op a) G.(e) p | _ => G.(e) end.
 Unset Implicit Arguments.
@@ -54,10 +54,10 @@ Theorem gpow_1 : gpow 1 = a.
 simpl; sauto.
 Qed.
 
-(************************************** 
+(**************************************
   Some properties of the power function
  **************************************)
- 
+
 Theorem gpow_in: forall n, In (gpow n) G.(s).
 intros n; case n; simpl; auto.
 intros p; apply iter_pos_invariant with (Inv := fun x => In x G.(s)); auto.
@@ -91,7 +91,7 @@ rewrite iter_pos_plus; rewrite (fun x y => gpow_op (iter_pos A x y p2)); auto.
 exact (gpow_in (Zpos p2)).
 Qed.
 
-Theorem gpow_1_more: 
+Theorem gpow_1_more:
   forall n, 0 < n -> gpow n = G.(e) -> forall m, 0 <= m -> exists p, 0 <= p < n /\ gpow m = gpow p.
 intros n H1 H2 m Hm;  generalize Hm; pattern m; apply Z_lt_induction; auto with zarith; clear m Hm.
 intros m Rec Hm.
@@ -110,7 +110,7 @@ apply g_cancel_l with (g:= G) (a := gpow n); sauto.
 rewrite <- gpow_add; try rewrite <- H3; sauto.
 Qed.
 
-(************************************** 
+(**************************************
   We build the support by iterating the power function
  **************************************)
 
@@ -118,21 +118,21 @@ Set Implicit Arguments.
 
 Fixpoint support_aux (b: A) (n: nat) {struct n}: list A :=
 b::let c := op a b in
-    match n with 
-       O => nil | 
-      (S n1) =>if A_dec c G.(e) then nil else  support_aux c n1 
+    match n with
+       O => nil |
+      (S n1) =>if A_dec c G.(e) then nil else  support_aux c n1
     end.
 
 Definition support := support_aux G.(e) (Zabs_nat (g_order G)).
 
 Unset Implicit Arguments.
 
-(************************************** 
+(**************************************
   Some properties of the support that helps to prove that we have a group
  **************************************)
 
-Theorem support_aux_gpow: 
-  forall n m b, 0 <=  m -> In b (support_aux (gpow m) n) -> 
+Theorem support_aux_gpow:
+  forall n m b, 0 <=  m -> In b (support_aux (gpow m) n) ->
         exists p, (0 <= p < length (support_aux (gpow m) n))%nat  /\ b = gpow (m + Z_of_nat p).
 intros n; elim n; simpl.
 intros n1 b Hm [H1 | H1]; exists 0%nat; simpl; rewrite Zplus_0_r; auto; case H1.
@@ -143,13 +143,13 @@ case H2.
 case (Rec (1 + m) b); auto with zarith.
 rewrite gpow_add; auto with zarith.
 rewrite gpow_1; auto.
-intros p (Hp1, Hp2); exists (S p); split; auto with zarith. 
+intros p (Hp1, Hp2); exists (S p); split; auto with zarith.
 rewrite <- gpow_1.
 rewrite <- gpow_add; auto with zarith.
 rewrite inj_S; rewrite Hp2; eq_tac; auto with zarith.
 Qed.
 
-Theorem gpow_support_aux_not_e: 
+Theorem gpow_support_aux_not_e:
   forall n m p, 0 <= m -> m < p < m + Z_of_nat (length (support_aux (gpow m) n)) -> gpow p <> G.(e).
 intros n; elim n; simpl.
 intros m p Hm (H1, H2); contradict H2; auto with zarith.
@@ -186,8 +186,8 @@ intros n; elim n; simpl; auto.
 intros n1 Rec a1; case (A_dec (op a a1) G.(e)); simpl; auto with arith.
 Qed.
 
-Theorem support_aux_length_le_is_e: 
-   forall n m, 0 <= m ->  (length (support_aux (gpow m) n) <= n)%nat -> 
+Theorem support_aux_length_le_is_e:
+   forall n m, 0 <= m ->  (length (support_aux (gpow m) n) <= n)%nat ->
       gpow (m + Z_of_nat (length (support_aux (gpow m) n))) = G.(e) .
 intros n; elim n; simpl; auto.
 intros m _ H1; contradict H1; auto with arith.
@@ -201,8 +201,8 @@ rewrite <- gpow_add; auto with zarith.
 rewrite  Zplus_assoc; rewrite (Zplus_comm 1); intros H2; apply Rec; auto with zarith.
 Qed.
 
-Theorem support_aux_in: 
-  forall n m p, 0 <= m ->  (p < length (support_aux (gpow m) n))% nat ->  
+Theorem support_aux_in:
+  forall n m p, 0 <= m ->  (p < length (support_aux (gpow m) n))% nat ->
             (In (gpow (m + Z_of_nat p)) (support_aux (gpow m) n)).
 intros n; elim n; simpl; auto; clear n.
 intros m p Hm H1; replace p with 0%nat.
@@ -224,7 +224,7 @@ rewrite <- gpow_1; rewrite <- gpow_add; auto with zarith.
 rewrite  Zplus_assoc; rewrite (Zplus_comm 1); intros H2; right; apply Rec; auto with zarith.
 Qed.
 
-Theorem support_aux_ulist: 
+Theorem support_aux_ulist:
   forall n m, 0 <= m -> (forall p, 0 <= p < m -> gpow (1 + p) <> G.(e)) -> ulist (support_aux (gpow m) n).
 intros n; elim n; auto; clear n.
 intros m _ _; auto.
@@ -338,13 +338,13 @@ apply inj_le_rev; rewrite inj_Zabs_nat; auto with zarith.
 rewrite Zabs_eq; auto with zarith.
 Qed.
 
-(************************************** 
+(**************************************
   We are now ready to build the group
  **************************************)
 
 Definition Gsupport: (FGroup op).
 generalize support_incl_G; unfold incl; intros Ho.
-apply mkGroup with support G.(e) G.(i); sauto. 
+apply mkGroup with support G.(e) G.(i); sauto.
 apply support_ulist.
 apply support_internal.
 intros a1 b1 c1 H1 H2 H3; apply G.(assoc); sauto.
@@ -352,7 +352,7 @@ apply support_in_e.
 apply support_i_internal.
 Defined.
 
-(************************************** 
+(**************************************
   Definition of the order of an element
  **************************************)
 Set Implicit Arguments.
@@ -361,7 +361,7 @@ Definition e_order := Z_of_nat (length support).
 
 Unset Implicit Arguments.
 
-(************************************** 
+(**************************************
  Some properties of the order of an element
  **************************************)
 
@@ -474,7 +474,7 @@ apply Zpower_ge_0; auto with zarith.
 Qed.
 
 Theorem gpow_mult: forall (A : Set) (op : A -> A -> A) (a b: A) (G : FGroup op)
-       (comm: forall a b,  In a (s G) -> In b (s G) -> op a b = op b a), 
+       (comm: forall a b,  In a (s G) -> In b (s G) -> op a b = op b a),
        In a (s G) -> In b (s G) -> forall n, 0 <= n -> gpow (op a b) G n = op (gpow a G n) (gpow b G n).
 intros A op a  b G comm Ha Hb n; case n; simpl; auto.
 intros _; rewrite G.(e_is_zero_r); auto.
@@ -504,8 +504,8 @@ case H4; intros q3 H5; exists q3; rewrite H2; rewrite H5; auto with zarith.
 Qed.
 
 Theorem order_mult: forall (A : Set) (op : A -> A -> A) (A_dec: forall a b: A, {a = b} + {~ a = b}) (G : FGroup op)
-       (comm: forall a b,  In a (s G) -> In b (s G) -> op a b = op b a) (a b: A), 
-       In a (s G) -> In b (s G) -> rel_prime (e_order A_dec a G) (e_order A_dec b G) -> 
+       (comm: forall a b,  In a (s G) -> In b (s G) -> op a b = op b a) (a b: A),
+       In a (s G) -> In b (s G) -> rel_prime (e_order A_dec a G) (e_order A_dec b G) ->
         e_order A_dec (op a b) G = e_order A_dec a G * e_order A_dec b G.
 intros A op A_dec G comm a b Ha Hb Hab.
 assert (Hoat: 0 < e_order A_dec a G); try apply e_order_pos.
@@ -576,10 +576,10 @@ case (e_order_divide_gpow A Adec op a G H1 m F1 H2); intros q Hq.
 assert (F2: 1 <= q).
   case (Zle_or_lt 0 q); intros HH.
     case (Zle_lt_or_eq _ _ HH); auto with zarith.
-    intros HH1; generalize Hm; rewrite Hq; rewrite <- HH1; 
+    intros HH1; generalize Hm; rewrite Hq; rewrite <- HH1;
       auto with zarith.
   assert (F2: 0 <= (- q) * e_order Adec a G); auto with zarith.
-    apply Zmult_le_0_compat; auto with zarith. 
+    apply Zmult_le_0_compat; auto with zarith.
     apply Zlt_le_weak; apply e_order_pos.
   generalize F2; rewrite Zopp_mult_distr_l_reverse;
       rewrite <- Hq; auto with zarith.
diff --git a/coqprime/Coqprime/Euler.v b/coqprime/Coqprime/Euler.v
index 06d92ce57..93f6956ba 100644
--- a/coqprime/Coqprime/Euler.v
+++ b/coqprime/Coqprime/Euler.v
@@ -20,7 +20,7 @@ Open Scope Z_scope.
 
 Definition phi n := Zsum 1 (n - 1) (fun x => if rel_prime_dec x n then 1 else 0).
 
-Theorem phi_def_with_0:  
+Theorem phi_def_with_0:
   forall n, 1< n -> phi n = Zsum 0 (n - 1) (fun x => if rel_prime_dec x n then 1 else 0).
 intros n H; rewrite Zsum_S_left; auto with zarith.
 case (rel_prime_dec 0 n); intros H2.
@@ -47,7 +47,7 @@ Qed.
 
 Theorem phi_le_n_minus_1: forall n, 1 < n -> phi n <= n - 1.
 intros n H; replace (n-1) with ((1 +  (n - 1) - 1) * 1); auto with zarith.
-rewrite <- Zsum_c; auto with zarith. 
+rewrite <- Zsum_c; auto with zarith.
 unfold phi; apply Zsum_le; auto with zarith.
 intros x H1; case (rel_prime_dec x n); auto with zarith.
 Qed.
@@ -59,7 +59,7 @@ assert (2 <= n); auto with zarith.
 apply prime_ge_2; auto.
 rewrite <- Zsum_c; auto with zarith; unfold phi; apply Zsum_ext; auto.
 intros x  (H2, H3); case H; clear H; intros H H1.
-generalize (H1 x); case (rel_prime_dec x n); auto with zarith. 
+generalize (H1 x); case (rel_prime_dec x n); auto with zarith.
 intros H6 H7; contradict H6; apply H7; split; auto with zarith.
 Qed.
 
diff --git a/coqprime/Coqprime/FGroup.v b/coqprime/Coqprime/FGroup.v
index a55710e7c..ee18761ab 100644
--- a/coqprime/Coqprime/FGroup.v
+++ b/coqprime/Coqprime/FGroup.v
@@ -7,22 +7,22 @@
 (*************************************************************)
 
 (**********************************************************************
-    FGroup.v                        
-                                                                     
-    Defintion and properties of finite groups                         
-                                                                     
-    Definition: FGroup              
+    FGroup.v
+
+    Defintion and properties of finite groups
+
+    Definition: FGroup
   **********************************************************************)
 Require Import List.
 Require Import UList.
 Require Import Tactic.
 Require Import ZArith.
 
-Open Scope Z_scope. 
+Open Scope Z_scope.
 
 Set Implicit Arguments.
 
-(************************************** 
+(**************************************
   A finite group is defined for an operation op
   it has a support  (s)
   op operates inside the group (internal)
@@ -32,7 +32,7 @@ Set Implicit Arguments.
   the inverse operates inside the group (i_internal)
   it gives an inverse (i_is_inverse_l is_is_inverse_r)
  **************************************)
- 
+
 Record FGroup (A: Set) (op: A -> A -> A): Set := mkGroup
   {s : (list A);
    unique_s: ulist s;
@@ -48,10 +48,10 @@ Record FGroup (A: Set) (op: A -> A -> A): Set := mkGroup
    i_is_inverse_r:  forall a, (In a s) -> op a (i a) = e
 }.
 
-(************************************** 
+(**************************************
    The order of a group is the lengh of the support
  **************************************)
- 
+
 Definition g_order  (A: Set) (op: A -> A -> A) (g: FGroup op)  := Z_of_nat (length g.(s)).
 
 Unset Implicit Arguments.
@@ -65,7 +65,7 @@ Section FGroup.
 Variable A: Set.
 Variable op: A -> A -> A.
 
-(************************************** 
+(**************************************
    Some properties of a finite group
  **************************************)
 
@@ -91,7 +91,7 @@ apply sym_equal; apply assoc with g; sauto.
 replace (op a (g.(i) a)) with g.(e); sauto.
 Qed.
 
-Theorem e_unique: forall (g : FGroup op), forall e1, In e1 g.(s) ->  (forall a, In a g.(s) -> op e1 a = a) -> e1 = g.(e). 
+Theorem e_unique: forall (g : FGroup op), forall e1, In e1 g.(s) ->  (forall a, In a g.(s) -> op e1 a = a) -> e1 = g.(e).
 intros g e1 He1 H2.
 apply trans_equal with (op e1 g.(e)); sauto.
 Qed.
@@ -110,7 +110,7 @@ intro g; apply g_cancel_l with (g:= g) (a := g.(e)); sauto.
 apply trans_equal with g.(e); sauto.
 Qed.
 
-(************************************** 
+(**************************************
    A group has at least one element
  **************************************)
 
diff --git a/coqprime/Coqprime/IGroup.v b/coqprime/Coqprime/IGroup.v
index 11a73d414..775596a71 100644
--- a/coqprime/Coqprime/IGroup.v
+++ b/coqprime/Coqprime/IGroup.v
@@ -7,11 +7,11 @@
 (*************************************************************)
 
 (**********************************************************************
-    Igroup                    
-                                                                     
+    Igroup
+
     Build the group of the inversible elements for the operation
-                                                              
-    Definition: ZpGroup              
+
+    Definition: ZpGroup
   **********************************************************************)
 Require Import ZArith.
 Require Import Tactic.
@@ -37,12 +37,12 @@ Hypothesis op_assoc: forall a b c, In a support -> In b support -> In c support
 Hypothesis e_is_zero_l:  forall a, In a support ->  op e a = a.
 Hypothesis e_is_zero_r:  forall a, In a support ->  op a e = a.
 
-(************************************** 
+(**************************************
   is_inv_aux tests if there is an inverse of a for op in l
  **************************************)
 
 Fixpoint is_inv_aux (l: list A) (a: A) {struct l}: bool :=
-  match l with nil => false | cons b l1 => 
+  match l with nil => false | cons b l1 =>
    if (A_dec (op a b) e) then if (A_dec (op b a) e) then true else is_inv_aux l1 a else is_inv_aux l1 a
   end.
 
@@ -52,19 +52,19 @@ intros a l1 Rec H; case (A_dec (op a b) e); case (A_dec (op b a) e); auto.
 intros H1 H2; case (H a); auto; intros H3; case H3; auto.
 Qed.
 
-(************************************** 
+(**************************************
   is_inv tests if there is an inverse in support
  **************************************)
 Definition is_inv := is_inv_aux support.
 
-(************************************** 
+(**************************************
   isupport_aux returns the sublist of inversible element of support
  **************************************)
 
 Fixpoint isupport_aux (l: list A) : list  A :=
   match l with nil => nil | cons a  l1 => if is_inv a then a::isupport_aux l1 else isupport_aux l1 end.
 
-(************************************** 
+(**************************************
   Some properties of isupport_aux
  **************************************)
 
@@ -82,7 +82,7 @@ case (is_inv b); auto with datatypes.
 Qed.
 
 
-Theorem isupport_aux_not_in: 
+Theorem isupport_aux_not_in:
   forall b l, (forall a, (In a support) -> op b a <> e \/  op a b <> e) -> ~ In b (isupport_aux l).
 intros b l; elim l; simpl; simpl; auto.
 intros a l1 H; case_eq (is_inv a); intros H1; simpl; auto.
@@ -107,13 +107,13 @@ apply H1; apply ulist_app_inv_r with (a:: nil); auto.
 apply H1; apply ulist_app_inv_r with (a:: nil); auto.
 Qed.
 
-(************************************** 
+(**************************************
   isupport is the sublist of inversible element of support
  **************************************)
 
 Definition isupport := isupport_aux support.
 
-(************************************** 
+(**************************************
   Some properties of isupport
  **************************************)
 
@@ -140,17 +140,17 @@ apply isupport_ulist.
 apply isupport_incl.
 Qed.
 
-Theorem isupport_length_strict:  
-  forall b, (In b support) -> (forall a, (In a support) -> op b a <> e \/  op a b <> e) -> 
+Theorem isupport_length_strict:
+  forall b, (In b support) -> (forall a, (In a support) -> op b a <> e \/  op a b <> e) ->
            (length isupport < length support)%nat.
 intros b H H1; apply ulist_incl_length_strict.
 apply isupport_ulist.
 apply isupport_incl.
 intros H2; case (isupport_aux_not_in b support); auto.
 Qed.
- 
+
 Fixpoint inv_aux (l: list A) (a: A) {struct l}: A :=
-  match l with nil => e | cons b l1 => 
+  match l with nil => e | cons b l1 =>
    if  A_dec (op a b) e then  if (A_dec (op b a) e) then b else inv_aux l1 a else inv_aux l1 a
   end.
 
@@ -180,25 +180,25 @@ intros l a; elim l; simpl; auto.
 intros b l1; case (A_dec (op a b) e); case (A_dec (op b a) e); intros _ _ [H1 | H1]; auto.
 Qed.
 
-(************************************** 
+(**************************************
   The inverse function
  **************************************)
 
 Definition inv := inv_aux support.
 
-(************************************** 
+(**************************************
   Some properties of inv
  **************************************)
 
 Theorem inv_prop_r: forall a, In a isupport -> op a (inv a) = e.
 intros a H; unfold inv; apply inv_aux_prop_r with (l := support).
-change (is_inv a = true). 
+change (is_inv a = true).
 apply isupport_is_inv_true; auto.
 Qed.
 
 Theorem inv_prop_l: forall a, In a isupport -> op (inv a) a = e.
 intros a H; unfold inv; apply inv_aux_prop_l with (l := support).
-change (is_inv a = true). 
+change (is_inv a = true).
 apply isupport_is_inv_true; auto.
 Qed.
 
@@ -220,8 +220,8 @@ case (inv_aux_in support a); unfold inv; auto.
 intros H1; rewrite H1; apply e_in_support; auto with zarith.
 Qed.
 
-(************************************** 
-   We are now ready to build our group 
+(**************************************
+   We are now ready to build our group
  **************************************)
 
 Definition IGroup : (FGroup op).
diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v
index 96d3e5655..dbfde2c38 100644
--- a/coqprime/Coqprime/Iterator.v
+++ b/coqprime/Coqprime/Iterator.v
@@ -9,7 +9,7 @@
 Require Export List.
 Require Export Permutation.
 Require Import Arith.
- 
+
 Section Iterator.
 Variables A B : Set.
 Variable zero : B.
@@ -18,17 +18,17 @@ Variable g : B -> B ->  B.
 Hypothesis g_zero : forall a,  g a zero = a.
 Hypothesis g_trans : forall a b c,  g a (g b c) = g (g a b) c.
 Hypothesis g_sym : forall a b,  g a b = g b a.
- 
+
 Definition iter := fold_right (fun a r => g (f a) r) zero.
 Hint Unfold iter .
- 
+
 Theorem iter_app: forall l1 l2,  iter (app l1 l2) = g (iter l1) (iter l2).
 intros l1; elim l1; simpl; auto.
 intros l2; rewrite g_sym; auto.
 intros a l H l2; rewrite H.
 rewrite g_trans; auto.
 Qed.
- 
+
 Theorem iter_permutation: forall l1 l2, permutation l1 l2 ->  iter l1 = iter l2.
 intros l1 l2 H; elim H; simpl; auto; clear H l1 l2.
 intros a l1 l2 H1 H2; apply f_equal2 with ( f := g ); auto.
@@ -36,7 +36,7 @@ intros a b l; (repeat rewrite g_trans).
 apply f_equal2 with ( f := g ); auto.
 intros l1 l2 l3 H H0 H1 H2; apply trans_equal with ( 1 := H0 ); auto.
 Qed.
- 
+
 Lemma iter_inv:
  forall P l,
  P zero ->
@@ -45,14 +45,14 @@ Lemma iter_inv:
 intros P l H H0; (elim l; simpl; auto).
 Qed.
 Variable next : A ->  A.
- 
+
 Fixpoint progression (m : A) (n : nat) {struct n} : list A :=
  match n with   0 => nil
                | S n1 => cons m (progression (next m) n1) end.
- 
+
 Fixpoint next_n (c : A) (n : nat) {struct n} : A :=
  match n with 0 => c | S n1 => next_n (next c) n1 end.
- 
+
 Theorem progression_app:
  forall a b n m,
  le m n ->
@@ -64,9 +64,9 @@ intros m H a b n; case n; simpl; clear n.
 intros H1; absurd (0 < 1 + m); auto with arith.
 intros n H0 H1; apply f_equal2 with ( f := @cons A ); auto with arith.
 Qed.
- 
+
 Let iter_progression := fun m n => iter (progression m n).
- 
+
 Theorem iter_progression_app:
  forall a b n m,
  le m n ->
@@ -76,11 +76,11 @@ Theorem iter_progression_app:
 intros a b n m H H0; unfold iter_progression; rewrite (progression_app a b n m);
  (try apply iter_app); auto.
 Qed.
- 
+
 Theorem length_progression: forall z n,  length (progression z n) = n.
 intros z n; generalize z; elim n; simpl; auto.
 Qed.
- 
+
 End Iterator.
 Implicit Arguments iter [A B].
 Implicit Arguments progression [A].
@@ -88,21 +88,21 @@ Implicit Arguments next_n [A].
 Hint Unfold iter .
 Hint Unfold progression .
 Hint Unfold next_n .
- 
+
 Theorem iter_ext:
  forall (A B : Set) zero (f1 : A ->  B) f2 g l,
  (forall a, In a l ->  f1 a = f2 a) ->  iter zero f1 g l = iter zero f2 g l.
 intros A B zero f1 f2 g l; elim l; simpl; auto.
 intros a l0 H H0; apply f_equal2 with ( f := g ); auto.
 Qed.
- 
+
 Theorem iter_map:
  forall (A B C : Set) zero (f : B ->  C) g (k : A ->  B) l,
   iter zero f g (map k l) = iter zero (fun x => f (k x)) g l.
 intros A B C zero f g k l; elim l; simpl; auto.
 intros; apply f_equal2 with ( f := g ); auto with arith.
 Qed.
- 
+
 Theorem iter_comp:
  forall (A B : Set) zero (f1 f2 : A ->  B) g l,
  (forall a,  g a zero = a) ->
@@ -115,7 +115,7 @@ intros a l0 H; rewrite <- H; (repeat rewrite <- g_trans).
 apply f_equal2 with ( f := g ); auto.
 (repeat rewrite g_trans); apply f_equal2 with ( f := g ); auto.
 Qed.
- 
+
 Theorem iter_com:
  forall (A B : Set) zero (f : A -> A ->  B) g l1 l2,
  (forall a,  g a zero = a) ->
@@ -142,7 +142,7 @@ apply f_equal2 with ( f := g ); auto.
 (repeat rewrite <- H0); auto.
 apply f_equal2 with ( f := g ); auto.
 Qed.
- 
+
 Theorem iter_comp_const:
  forall (A B : Set) zero (f : A ->  B) g k l,
  k zero = zero ->
@@ -151,14 +151,14 @@ Theorem iter_comp_const:
 intros A B zero f g k l H H0; elim l; simpl; auto.
 intros a l0 H1; rewrite H0; apply f_equal2 with ( f := g ); auto.
 Qed.
- 
+
 Lemma next_n_S: forall n m,  next_n S n m = plus n m.
 intros n m; generalize n; elim m; clear n m; simpl; auto with arith.
 intros m H n; case n; simpl; auto with arith.
 rewrite H; auto with arith.
 intros n1; rewrite H; simpl; auto with arith.
 Qed.
- 
+
 Theorem progression_S_le_init:
  forall n m p, In p (progression S n m) ->  le n p.
 intros n m; generalize n; elim m; clear n m; simpl; auto.
@@ -167,7 +167,7 @@ intros m H n p [H1|H1]; auto with arith.
 subst n; auto.
 apply le_S_n; auto with arith.
 Qed.
- 
+
 Theorem progression_S_le_end:
  forall n m p, In p (progression S n m) ->  lt p (n + m).
 intros n m; generalize n; elim m; clear n m; simpl; auto.
diff --git a/coqprime/Coqprime/Lagrange.v b/coqprime/Coqprime/Lagrange.v
index b35460bad..4765c76c4 100644
--- a/coqprime/Coqprime/Lagrange.v
+++ b/coqprime/Coqprime/Lagrange.v
@@ -7,12 +7,12 @@
 (*************************************************************)
 
 (**********************************************************************
-    Lagrange.v                        
-                                                                     
-    Proof of Lagrange theorem: 
-      the oder of a subgroup divides the order of a group                         
-                                                                     
-    Definition: lagrange              
+    Lagrange.v
+
+    Proof of Lagrange theorem:
+      the oder of a subgroup divides the order of a group
+
+    Definition: lagrange
   **********************************************************************)
 Require Import List.
 Require Import UList.
@@ -37,7 +37,7 @@ Variable H:(FGroup op).
 
 Hypothesis G_in_H: (incl G.(s)  H.(s)).
 
-(************************************** 
+(**************************************
    A group and a subgroup have the same neutral element
  **************************************)
 
@@ -53,11 +53,11 @@ apply trans_equal with (op G.(e) H.(e)); sauto.
 eq_tac; sauto.
 Qed.
 
-(************************************** 
+(**************************************
    The proof works like this.
    If G = {e, g1, g2, g3, .., gn} and {e, h1, h2, h3, ..., hm}
    we construct the list mkGH
-    {e, g1, g2, g3, ...., gn 
+    {e, g1, g2, g3, ...., gn
      hi*e, hi * g1, hi * g2, ..., hi * gn   if hi does not appear before
      ....
      hk*e, hk * g1, hk * g2, ..., hk * gn   if hk does not appear before
@@ -67,16 +67,16 @@ Qed.
  **************************************)
 
 Fixpoint mkList (base l: (list A)) { struct l}  : (list A) :=
-  match l with 
+  match l with
    nil => nil
  | cons a l1 => let r1 := mkList base l1 in
-                         if (In_dec A_dec a r1) then r1 else 
+                         if (In_dec A_dec a r1) then r1 else
                           (map (op a) base) ++ r1
   end.
 
 Definition mkGH := mkList G.(s) H.(s).
 
-Theorem mkGH_length:  divide (length G.(s)) (length mkGH). 
+Theorem mkGH_length:  divide (length G.(s)) (length mkGH).
 unfold mkGH; elim H.(s); simpl.
 exists 0%nat; auto with arith.
 intros a l1 (c, H1); case (In_dec A_dec a (mkList  G.(s) l1)); intros H2.
@@ -161,11 +161,11 @@ assert (In a H.(s)); sauto; apply (H2 a); auto with datatypes.
 unfold mkGH; apply H1; auto with datatypes.
 Qed.
 
-(************************************** 
+(**************************************
   Lagrange theorem
  **************************************)
- 
-Theorem lagrange: (g_order G | (g_order H)). 
+
+Theorem lagrange: (g_order G | (g_order H)).
 unfold g_order.
 rewrite Permutation.permutation_length with  (l := H.(s)) (m:= mkGH).
 case mkGH_length; intros x H1; exists (Z_of_nat x).
diff --git a/coqprime/Coqprime/ListAux.v b/coqprime/Coqprime/ListAux.v
index c3c9602bd..2443faf52 100644
--- a/coqprime/Coqprime/ListAux.v
+++ b/coqprime/Coqprime/ListAux.v
@@ -7,9 +7,9 @@
 (*************************************************************)
 
 (**********************************************************************
-     Aux.v                                                                                           
-                                                                                                          
-     Auxillary functions & Theorems                                              
+     Aux.v
+
+     Auxillary functions & Theorems
   **********************************************************************)
 Require Export List.
 Require Export Arith.
@@ -17,18 +17,18 @@ Require Export Tactic.
 Require Import Inverse_Image.
 Require Import Wf_nat.
 
-(************************************** 
+(**************************************
    Some properties on list operators: app, map,...
 **************************************)
- 
+
 Section List.
 Variables (A : Set) (B : Set) (C : Set).
 Variable f : A ->  B.
 
-(************************************** 
-  An induction theorem for list based on length 
+(**************************************
+  An induction theorem for list based on length
 **************************************)
- 
+
 Theorem list_length_ind:
  forall (P : list A ->  Prop),
  (forall (l1 : list A),
@@ -40,7 +40,7 @@ intros P H l;
 apply wf_inverse_image with ( R := lt ); auto.
 apply lt_wf.
 Qed.
- 
+
 Definition list_length_induction:
  forall (P : list A ->  Set),
  (forall (l1 : list A),
@@ -52,7 +52,7 @@ intros P H l;
 apply wf_inverse_image with ( R := lt ); auto.
 apply lt_wf.
 Qed.
- 
+
 Theorem in_ex_app:
  forall (a : A) (l : list A),
  In a l ->  (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2)  ).
@@ -66,20 +66,20 @@ rewrite Hl2; auto.
 Qed.
 
 (**************************************
- Properties on app 
+ Properties on app
 **************************************)
- 
+
 Theorem length_app:
  forall (l1 l2 : list A),  length (l1 ++ l2) = length l1 + length l2.
 intros l1; elim l1; simpl; auto.
 Qed.
- 
+
 Theorem app_inv_head:
  forall (l1 l2 l3 : list A), l1 ++ l2 = l1 ++ l3 ->  l2 = l3.
 intros l1; elim l1; simpl; auto.
 intros a l H l2 l3 H0; apply H; injection H0; auto.
 Qed.
- 
+
 Theorem app_inv_tail:
  forall (l1 l2 l3 : list A), l2 ++ l1 = l3 ++ l1 ->  l2 = l3.
 intros l1 l2; generalize l1; elim l2; clear l1 l2; simpl; auto.
@@ -94,7 +94,7 @@ rewrite H1; auto with arith.
 simpl; intros b l0 H0; injection H0.
 intros H1 H2; rewrite H2, (H _ _ H1); auto.
 Qed.
- 
+
 Theorem app_inv_app:
  forall l1 l2 l3 l4 a,
  l1 ++ l2 = l3 ++ (a :: l4) ->
@@ -109,7 +109,7 @@ injection H0; auto.
 intros [l5 H1].
 left; exists l5; injection H0; intros; subst; auto.
 Qed.
- 
+
 Theorem app_inv_app2:
  forall l1 l2 l3 l4 a b,
  l1 ++ l2 = l3 ++ (a :: (b :: l4)) ->
@@ -129,7 +129,7 @@ intros [l5 HH1]; left; exists l5; injection H0; intros; subst; auto.
 intros [H1|[H1 H2]]; auto.
 right; right; split; auto; injection H0; intros; subst; auto.
 Qed.
- 
+
 Theorem same_length_ex:
  forall (a : A) l1 l2 l3,
  length (l1 ++ (a :: l2)) = length l3 ->
@@ -148,10 +148,10 @@ exists (b :: l4); exists l5; exists b1; (repeat (simpl; split; auto)).
 rewrite HH3; auto.
 Qed.
 
-(************************************** 
-  Properties on map 
+(**************************************
+  Properties on map
 **************************************)
- 
+
 Theorem in_map_inv:
  forall (b : B) (l : list A),
  In b (map f l) ->  (exists a : A , In a l /\ b = f a ).
@@ -161,7 +161,7 @@ intros a0 l0 H [H1|H1]; auto.
 exists a0; auto.
 case (H H1); intros a1 [H2 H3]; exists a1; auto.
 Qed.
- 
+
 Theorem in_map_fst_inv:
  forall a (l : list (B * C)),
  In a (map (fst (B:=_)) l) ->  (exists c , In (a, c) l ).
@@ -171,16 +171,16 @@ intros a0 l0 H [H0|H0]; auto.
 exists (snd a0); left; rewrite <- H0; case a0; simpl; auto.
 case H; auto; intros l1 Hl1; exists l1; auto.
 Qed.
- 
+
 Theorem length_map: forall l,  length (map f l) = length l.
 intros l; elim l; simpl; auto.
 Qed.
- 
+
 Theorem map_app: forall l1 l2,  map f (l1 ++ l2) = map f l1 ++ map f l2.
 intros l; elim l; simpl; auto.
 intros a l0 H l2; rewrite H; auto.
 Qed.
- 
+
 Theorem map_length_decompose:
  forall l1 l2 l3 l4,
  length l1 = length l2 ->
@@ -197,10 +197,10 @@ intros H4 H5; split; auto.
 subst; auto.
 Qed.
 
-(************************************** 
-  Properties of flat_map 
+(**************************************
+  Properties of flat_map
 **************************************)
- 
+
 Theorem in_flat_map:
  forall (l : list B) (f : B ->  list C) a b,
  In a (f b) -> In b l ->  In a (flat_map f l).
@@ -209,7 +209,7 @@ intros a l0 H a0 b H0 [H1|H1]; apply in_or_app; auto.
 left; rewrite H1; auto.
 right; apply H with ( b := b ); auto.
 Qed.
- 
+
 Theorem in_flat_map_ex:
  forall (l : list B) (f : B ->  list C) a,
  In a (flat_map f l) ->  (exists b , In b l /\ In a (f b) ).
@@ -221,17 +221,17 @@ intros H1; case H with ( 1 := H1 ).
 intros b [H2 H3]; exists b; simpl; auto.
 Qed.
 
-(************************************** 
-  Properties of fold_left 
+(**************************************
+  Properties of fold_left
 **************************************)
 
-Theorem fold_left_invol: 
+Theorem fold_left_invol:
   forall (f: A -> B -> A) (P: A -> Prop) l a,
   P a ->  (forall x y, P x -> P (f x y)) -> P (fold_left f l a).
 intros f1 P l; elim l; simpl; auto.
-Qed. 
+Qed.
 
-Theorem fold_left_invol_in: 
+Theorem fold_left_invol_in:
   forall (f: A -> B -> A) (P: A -> Prop) l a b,
   In b l -> (forall x, P (f x b)) -> (forall x y, P x -> P (f x y)) ->
   P (fold_left f l a).
@@ -245,17 +245,17 @@ Qed.
 End List.
 
 
-(************************************** 
+(**************************************
   Propertie of list_prod
 **************************************)
- 
+
 Theorem length_list_prod:
  forall (A : Set) (l1 l2 : list A),
   length (list_prod l1 l2) = length l1 * length l2.
 intros A l1 l2; elim l1; simpl; auto.
 intros a l H; rewrite length_app; rewrite length_map; rewrite H; auto.
 Qed.
- 
+
 Theorem in_list_prod_inv:
  forall (A B : Set) a l1 l2,
  In a (list_prod l1 l2) ->
diff --git a/coqprime/Coqprime/LucasLehmer.v b/coqprime/Coqprime/LucasLehmer.v
index a0e3b8e46..6e3d218f2 100644
--- a/coqprime/Coqprime/LucasLehmer.v
+++ b/coqprime/Coqprime/LucasLehmer.v
@@ -7,11 +7,11 @@
 (*************************************************************)
 
 (**********************************************************************
-    LucasLehamer.v                        
-                                                                     
+    LucasLehamer.v
+
     Build the sequence for the primality test of Mersenne numbers
-                                                                 
-    Definition: LucasLehmer              
+
+    Definition: LucasLehmer
   **********************************************************************)
 Require Import ZArith.
 Require Import ZCAux.
@@ -27,7 +27,7 @@ Require Import IGroup.
 
 Open Scope Z_scope.
 
-(************************************** 
+(**************************************
   The seeds of the serie
  **************************************)
 
@@ -43,13 +43,13 @@ Theorem w_mult_v : pmult w v = (1, 0).
 simpl; auto.
 Qed.
 
-(************************************** 
+(**************************************
   Definition of the power function for pairs p^n
  **************************************)
 
 Definition ppow p n := match n with  Zpos q => iter_pos _ (pmult p) (1, 0) q | _ => (1, 0) end.
 
-(************************************** 
+(**************************************
   Some properties of ppow
  **************************************)
 
@@ -66,7 +66,7 @@ Qed.
 Theorem ppow_op: forall a b p, iter_pos _ (pmult a) b p = pmult (iter_pos _ (pmult a) (1, 0) p) b.
 intros a b p; generalize b; elim p; simpl; auto; clear  b p.
 intros p Rec b.
-rewrite (Rec b). 
+rewrite (Rec b).
 try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto.
 repeat rewrite pmult_assoc; auto.
 intros p Rec b.
@@ -118,13 +118,13 @@ rewrite (fun x y => pmult_comm (iter_pos _ x y p3) p); auto.
 rewrite (pmult_assoc m); try apply pmult_comm; auto.
 Qed.
 
-(************************************** 
+(**************************************
   We can now define our series of pairs s
  **************************************)
 
 Definition s n := pplus (ppow w (2 ^ n)) (ppow v (2 ^ n)).
 
-(************************************** 
+(**************************************
   Some properties of s
  **************************************)
 
@@ -149,7 +149,7 @@ repeat rewrite <- ppow_mult; auto with zarith.
 rewrite (pmult_comm v w); rewrite w_mult_v.
 rewrite ppow_1.
 repeat rewrite tpower_1.
-rewrite pplus_comm; repeat rewrite <- pplus_assoc; 
+rewrite pplus_comm; repeat rewrite <- pplus_assoc;
 rewrite pplus_comm; repeat rewrite <- pplus_assoc.
 simpl; case (ppow (7, -4) (2 ^n)); simpl; intros z1 z2; eq_tac; auto with zarith.
 Qed.
@@ -201,7 +201,7 @@ Section Lucas.
 
 Variable p: Z.
 
-(************************************** 
+(**************************************
   Definition of the mersenne number
  **************************************)
 
@@ -216,7 +216,7 @@ Qed.
 
 Hypothesis p_pos2: 2 < p.
 
-(************************************** 
+(**************************************
   We suppose that the mersenne number divides s
  **************************************)
 
@@ -224,7 +224,7 @@ Hypothesis Mp_divide_sn: (Mp  | fst (s (p - 2))).
 
 Variable q: Z.
 
-(************************************** 
+(**************************************
   We take a divisor of Mp and shows that Mp <= q^2, hence Mp is prime
  **************************************)
 
@@ -236,7 +236,7 @@ Theorem q_pos: 1 < q.
 apply Zlt_trans with (2 := q_pos2); auto with zarith.
 Qed.
 
-(************************************** 
+(**************************************
   The definition of the groups of inversible pairs
  **************************************)
 
@@ -285,18 +285,18 @@ intros a _; left; rewrite zpmult_0_l; auto with zarith.
 intros; discriminate.
 Qed.
 
-(************************************** 
+(**************************************
   The power function zpow: a^n
  **************************************)
 
-Definition zpow a := gpow a pgroup. 
+Definition zpow a := gpow a pgroup.
 
-(************************************** 
+(**************************************
   Some properties of zpow
  **************************************)
 
-Theorem zpow_def: 
-  forall a b, In a pgroup.(FGroup.s) -> 0 <= b -> 
+Theorem zpow_def:
+  forall a b, In a pgroup.(FGroup.s) -> 0 <= b ->
      zpow a b = ((fst (ppow a b)) mod q, (snd (ppow a b)) mod q).
 generalize q_pos; intros HM.
 generalize q_pos2; intros HM2.
@@ -362,7 +362,7 @@ rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith.
 unfold zpow; rewrite gpow_gpow; auto with zarith.
 generalize zpow_w_n_minus_1; unfold zpow; intros H1; rewrite H1; clear H1.
 simpl; unfold zpmult, pmult.
-repeat (rewrite Zmult_0_l || rewrite Zmult_0_r || rewrite Zplus_0_l || 
+repeat (rewrite Zmult_0_l || rewrite Zmult_0_r || rewrite Zplus_0_l ||
               rewrite Zplus_0_r || rewrite Zmult_1_r).
 eq_tac; auto.
 pattern (-1 mod q) at 1; rewrite <- (Zmod_mod (-1) q); auto with zarith.
@@ -371,7 +371,7 @@ rewrite Zmod_small; auto with zarith.
 apply w_in_pgroup.
 Qed.
 
-(************************************** 
+(**************************************
   As e = (1, 0), the previous equation implies that the order of the group divide 2^p
  **************************************)
 
@@ -385,7 +385,7 @@ apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith.
 exact zpow_w_n.
 Qed.
 
-(************************************** 
+(**************************************
   So it is less than equal
  **************************************)
 
@@ -396,19 +396,19 @@ apply Zpower_gt_0; auto with zarith.
 apply e_order_divide_pow.
 Qed.
 
-(************************************** 
+(**************************************
   So order(w) must be 2^q
  **************************************)
 
 Theorem e_order_eq_pow:  exists q, (e_order P_dec w pgroup)  = 2 ^ q.
-case (Zdivide_power_2 (e_order P_dec w pgroup) 2 p); auto with zarith. 
+case (Zdivide_power_2 (e_order P_dec w pgroup) 2 p); auto with zarith.
 apply Zlt_le_weak; apply e_order_pos.
 apply prime_2.
 apply e_order_divide_pow; auto.
 intros x H; exists x; auto with zarith.
 Qed.
 
-(************************************** 
+(**************************************
   Buth this q can only be p otherwise it would contradict w^2^(p -1) = (-1, 0)
  **************************************)
 
@@ -449,7 +449,7 @@ apply (gpow_e_order_is_e _ P_dec _ w pgroup).
 apply w_in_pgroup.
 Qed.
 
-(************************************** 
+(**************************************
   We have then the expected conclusion
  **************************************)
 
@@ -483,7 +483,7 @@ Qed.
 
 End Lucas.
 
-(************************************** 
+(**************************************
   We build the sequence in Z
  **************************************)
 
@@ -494,7 +494,7 @@ Definition SS p :=
   | _ => (Zmodd 4 n)
   end.
 
-Theorem SS_aux_correct: 
+Theorem SS_aux_correct:
   forall p z1 z2 n, 0 <= n -> 0 < z1 -> z2 = fst (s n) mod z1 ->
         iter_pos _ (fun x => Zmodd (Zsquare x - 2) z1) z2 p = fst (s (n + Zpos p)) mod z1.
 intros p; pattern p; apply Pind.
@@ -558,7 +558,7 @@ pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith.
 replace (p - 1 + 1) with p; auto with zarith.
 Qed.
 
-(************************************** 
+(**************************************
   The test
  **************************************)
 
@@ -594,4 +594,3 @@ Qed.
 Theorem prime524287: prime 524287.
 exact (LucasTest 19 (refl_equal _)).
 Qed.
-
diff --git a/coqprime/Coqprime/NatAux.v b/coqprime/Coqprime/NatAux.v
index eab09150c..71d90cf9f 100644
--- a/coqprime/Coqprime/NatAux.v
+++ b/coqprime/Coqprime/NatAux.v
@@ -7,9 +7,9 @@
 (*************************************************************)
 
 (**********************************************************************
-     Aux.v                                                                                           
-                                                                                                          
-     Auxillary functions & Theorems                                              
+     Aux.v
+
+     Auxillary functions & Theorems
  **********************************************************************)
 Require Export Arith.
 
@@ -24,7 +24,7 @@ Qed.
 
 
 (**************************************
-  Definitions and properties of the power for nat 
+  Definitions and properties of the power for nat
 **************************************)
 
 Fixpoint pow (n m: nat)  {struct m} : nat := match m with O => 1%nat | (S m1) => (n * pow n m1)%nat  end.
@@ -56,7 +56,7 @@ apply pow_pos; auto with arith.
 Qed.
 
 (************************************
-  Definition of the divisibility for nat 
+  Definition of the divisibility for nat
 **************************************)
 
 Definition divide a b := exists c, b = a * c.
diff --git a/coqprime/Coqprime/PGroup.v b/coqprime/Coqprime/PGroup.v
index e9c1b2f47..5d8dc5d35 100644
--- a/coqprime/Coqprime/PGroup.v
+++ b/coqprime/Coqprime/PGroup.v
@@ -7,12 +7,12 @@
 (*************************************************************)
 
 (**********************************************************************
-    PGroup.v                        
-                                                                     
+    PGroup.v
+
     Build the group of pairs modulo needed for the theorem of
       lucas lehmer
-                                                                 
-    Definition: PGroup              
+
+    Definition: PGroup
  **********************************************************************)
 Require Import ZArith.
 Require Import Znumtheory.
@@ -29,7 +29,7 @@ Open Scope Z_scope.
 Definition base := 3.
 
 
-(************************************** 
+(**************************************
   Equality is decidable on pairs
  **************************************)
 
@@ -42,13 +42,13 @@ right; contradict H1; injection H1; auto.
 Defined.
 
 
-(************************************** 
+(**************************************
   Addition of two pairs
  **************************************)
 
 Definition pplus (p q: Z * Z) := let (x ,y) := p in let (z,t) := q in (x + z, y + t).
 
-(************************************** 
+(**************************************
   Properties of addition
  **************************************)
 
@@ -62,13 +62,13 @@ intros p q; case p; case q; intros q1 q2 p1 p2; unfold pplus.
 eq_tac; ring.
 Qed.
 
-(************************************** 
+(**************************************
   Multiplication of two pairs
  **************************************)
 
 Definition pmult (p q: Z * Z) := let (x ,y) := p in let (z,t) := q in (x * z + base * y * t, x * t + y * z).
 
-(************************************** 
+(**************************************
   Properties of multiplication
  **************************************)
 
@@ -109,7 +109,7 @@ intros p q r; case p; case q; case r; intros r1 r2 q1 q2 p1 p2; unfold pplus, pm
 eq_tac; ring.
 Qed.
 
-(************************************** 
+(**************************************
   In this section we create the group PGroup of inversible elements {(p, q) | 0 <= p < m /\ 0 <= q < m}
  **************************************)
 Section Mod.
@@ -118,14 +118,14 @@ Variable m : Z.
 
 Hypothesis m_pos: 1 < m.
 
-(************************************** 
+(**************************************
   mkLine creates {(a, p) | 0 <= p < n}
  **************************************)
 
 Fixpoint mkLine (a: Z) (n: nat) {struct n} : list (Z * Z) :=
-  (a, Z_of_nat n) :: match n with O => nil | (S n1) => mkLine a n1 end. 
+  (a, Z_of_nat n) :: match n with O => nil | (S n1) => mkLine a n1 end.
 
-(************************************** 
+(**************************************
   Some properties of mkLine
  **************************************)
 
@@ -165,14 +165,14 @@ intros x ((H2, H3), H4); injection H4.
 intros H5; subst; auto with zarith.
 Qed.
 
-(************************************** 
+(**************************************
   mkRect creates the list  {(p, q) | 0 <= p < n /\ 0 <= q < m}
  **************************************)
 
 Fixpoint mkRect (n m: nat) {struct n} : list (Z * Z) :=
-  (mkLine (Z_of_nat n) m) ++ match n with O => nil | (S n1) => mkRect n1 m end. 
+  (mkLine (Z_of_nat n) m) ++ match n with O => nil | (S n1) => mkRect n1 m end.
 
-(************************************** 
+(**************************************
   Some properties of mkRect
  **************************************)
 
@@ -221,12 +221,12 @@ change (~ Z_of_nat (S n1) <= Z_of_nat  n1).
 rewrite inj_S; auto with zarith.
 Qed.
 
-(************************************** 
+(**************************************
   mL is the list  {(p, q) | 0 <= p < m-1 /\ 0 <= q < m - 1}
  **************************************)
 Definition mL := mkRect (Zabs_nat (m - 1)) (Zabs_nat (m -1)).
 
-(************************************** 
+(**************************************
   Some properties of mL
  **************************************)
 
@@ -237,7 +237,7 @@ eq_tac; auto with zarith.
 Qed.
 
 Theorem mL_in: forall p q, 0 <= p < m -> 0 <= q <  m -> (In (p, q) mL).
-intros p q (H1, H2) (H3, H4); unfold mL; apply mkRect_in; rewrite inj_Zabs_nat; 
+intros p q (H1, H2) (H3, H4); unfold mL; apply mkRect_in; rewrite inj_Zabs_nat;
   rewrite Zabs_eq; auto with zarith.
 Qed.
 
@@ -251,13 +251,13 @@ Theorem mL_ulist:  ulist mL.
 unfold mL; apply mkRect_ulist; auto.
 Qed.
 
-(************************************** 
+(**************************************
   We define zpmult the multiplication of pairs module m
  **************************************)
 
 Definition zpmult (p q: Z * Z) := let (x ,y) := pmult p q in (Zmod x m, Zmod y m).
 
-(************************************** 
+(**************************************
   Some properties of zpmult
  **************************************)
 
@@ -329,8 +329,8 @@ Theorem zpmult_comm: forall p q, zpmult p q = zpmult q p.
 intros p q; unfold zpmult; rewrite pmult_comm; auto.
 Qed.
 
-(************************************** 
-   We are now ready to build our group 
+(**************************************
+   We are now ready to build our group
  **************************************)
 
 Definition PGroup : (FGroup zpmult).
diff --git a/coqprime/Coqprime/Permutation.v b/coqprime/Coqprime/Permutation.v
index a06693f89..3a9b0860e 100644
--- a/coqprime/Coqprime/Permutation.v
+++ b/coqprime/Coqprime/Permutation.v
@@ -7,20 +7,20 @@
 (*************************************************************)
 
 (**********************************************************************
-    Permutation.v                        
-                                                                     
-    Defintion and properties of permutations                         
+    Permutation.v
+
+    Defintion and properties of permutations
    **********************************************************************)
 Require Export List.
 Require Export ListAux.
- 
+
 Section permutation.
 Variable A : Set.
 
-(************************************** 
+(**************************************
    Definition of permutations as sequences of adjacent transpositions
  **************************************)
- 
+
 Inductive permutation : list A -> list A -> Prop :=
   | permutation_nil : permutation nil nil
   | permutation_skip :
@@ -33,10 +33,10 @@ Inductive permutation : list A -> list A -> Prop :=
       permutation l1 l2 -> permutation l2 l3 -> permutation l1 l3.
 Hint Constructors permutation.
 
-(************************************** 
+(**************************************
    Reflexivity
  **************************************)
- 
+
 Theorem permutation_refl : forall l : list A, permutation l l.
 simple induction l.
 apply permutation_nil.
@@ -45,10 +45,10 @@ apply permutation_skip with (1 := H).
 Qed.
 Hint Resolve permutation_refl.
 
-(************************************** 
+(**************************************
    Symmetry
    **************************************)
- 
+
 Theorem permutation_sym :
  forall l m : list A, permutation l m -> permutation m l.
 intros l1 l2 H'; elim H'.
@@ -61,10 +61,10 @@ intros l1' l2' l3' H1 H2 H3 H4.
 apply permutation_trans with (1 := H4) (2 := H2).
 Qed.
 
-(************************************** 
+(**************************************
    Compatibility with list length
    **************************************)
- 
+
 Theorem permutation_length :
  forall l m : list A, permutation l m -> length l = length m.
 intros l m H'; elim H'; simpl in |- *; auto.
@@ -72,20 +72,20 @@ intros l1 l2 l3 H'0 H'1 H'2 H'3.
 rewrite <- H'3; auto.
 Qed.
 
-(************************************** 
+(**************************************
    A permutation of the nil list is the nil list
    **************************************)
- 
+
 Theorem permutation_nil_inv : forall l : list A, permutation l nil -> l = nil.
 intros l H; generalize (permutation_length _ _ H); case l; simpl in |- *;
  auto.
 intros; discriminate.
 Qed.
- 
-(************************************** 
+
+(**************************************
    A permutation of the singleton list is the singleton list
    **************************************)
- 
+
 Let permutation_one_inv_aux :
   forall l1 l2 : list A,
   permutation l1 l2 -> forall a : A, l1 = a :: nil -> l2 = a :: nil.
@@ -101,19 +101,19 @@ Theorem permutation_one_inv :
 intros a l H; apply permutation_one_inv_aux with (l1 := a :: nil); auto.
 Qed.
 
-(************************************** 
+(**************************************
    Compatibility with the belonging
    **************************************)
- 
+
 Theorem permutation_in :
  forall (a : A) (l m : list A), permutation l m -> In a l -> In a m.
 intros a l m H; elim H; simpl in |- *; auto; intuition.
 Qed.
 
-(************************************** 
+(**************************************
    Compatibility with the append function
    **************************************)
- 
+
 Theorem permutation_app_comp :
  forall l1 l2 l3 l4,
  permutation l1 l2 -> permutation l3 l4 -> permutation (l1 ++ l3) (l2 ++ l4).
@@ -128,10 +128,10 @@ apply permutation_trans with (l2 ++ l4); auto.
 Qed.
 Hint Resolve permutation_app_comp.
 
-(************************************** 
+(**************************************
    Swap two sublists
    **************************************)
- 
+
 Theorem permutation_app_swap :
  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
 intros l1; elim l1; auto.
@@ -152,10 +152,10 @@ apply (app_ass l2 (a :: nil) l).
 apply (app_ass l2 (a :: nil) l).
 Qed.
 
-(************************************** 
+(**************************************
    A transposition is a permutation
    **************************************)
- 
+
 Theorem permutation_transposition :
  forall a b l1 l2 l3,
  permutation (l1 ++ a :: l2 ++ b :: l3) (l1 ++ b :: l2 ++ a :: l3).
@@ -173,10 +173,10 @@ apply permutation_app_comp; auto.
 apply permutation_app_swap; auto.
 Qed.
 
-(************************************** 
+(**************************************
    An element of a list can be put on top of the list to get a permutation
    **************************************)
- 
+
 Theorem in_permutation_ex :
  forall a l, In a l -> exists l1 : list A, permutation (a :: l1) l.
 intros a l; elim l; simpl in |- *; auto.
@@ -186,8 +186,8 @@ exists l0; rewrite H0; auto.
 case H; auto; intros l1 Hl1; exists (a0 :: l1).
 apply permutation_trans with (a0 :: a :: l1); auto.
 Qed.
- 
-(************************************** 
+
+(**************************************
    A permutation of a cons can be inverted
    **************************************)
 
@@ -232,7 +232,7 @@ intros l6 (l7, (Hl3, Hl4)).
 exists l6; exists l7; split; auto.
 apply permutation_trans with (1 := Hl2); auto.
 Qed.
- 
+
 Theorem permutation_cons_ex :
  forall (a : A) (l1 l2 : list A),
  permutation (a :: l1) l2 ->
@@ -242,10 +242,10 @@ intros a l1 l2 H.
 apply (permutation_cons_ex_aux a (a :: l1) l2 H nil l1); simpl in |- *; auto.
 Qed.
 
-(************************************** 
+(**************************************
    A permutation can be simply inverted if the two list starts with a cons
    **************************************)
- 
+
 Theorem permutation_inv :
  forall (a : A) (l1 l2 : list A),
  permutation (a :: l1) (a :: l2) -> permutation l1 l2.
@@ -260,11 +260,11 @@ apply permutation_skip; apply permutation_app_swap.
 apply (permutation_app_swap (a0 :: l4) l5).
 Qed.
 
-(************************************** 
-   Take a list and return tle list of all pairs of an element of the 
+(**************************************
+   Take a list and return tle list of all pairs of an element of the
    list and the remaining list
    **************************************)
- 
+
 Fixpoint split_one (l : list A) : list (A * list A) :=
   match l with
   | nil => nil (A:=A * list A)
@@ -273,10 +273,10 @@ Fixpoint split_one (l : list A) : list (A * list A) :=
       :: map (fun p : A * list A => (fst p, a :: snd p)) (split_one l1)
   end.
 
-(************************************** 
+(**************************************
    The pairs of the list are a permutation
    **************************************)
- 
+
 Theorem split_one_permutation :
  forall (a : A) (l1 l2 : list A),
  In (a, l1) (split_one l2) -> permutation (a :: l1) l2.
@@ -294,10 +294,10 @@ apply H2; auto.
 case a1; simpl in |- *; auto.
 Qed.
 
-(************************************** 
+(**************************************
    All elements of the list are there
    **************************************)
- 
+
 Theorem split_one_in_ex :
  forall (a : A) (l1 : list A),
  In a l1 -> exists l2 : list A, In (a, l2) (split_one l1).
@@ -312,10 +312,10 @@ apply
  auto.
 Qed.
 
-(************************************** 
+(**************************************
    An auxillary function to generate all permutations
    **************************************)
- 
+
 Fixpoint all_permutations_aux (l : list A) (n : nat) {struct n} :
  list (list A) :=
   match n with
@@ -326,13 +326,13 @@ Fixpoint all_permutations_aux (l : list A) (n : nat) {struct n} :
          map (cons (fst p)) (all_permutations_aux (snd p) n1)) (
         split_one l)
   end.
-(************************************** 
+(**************************************
    Generate all the permutations
    **************************************)
- 
+
 Definition all_permutations (l : list A) := all_permutations_aux l (length l).
- 
-(************************************** 
+
+(**************************************
    All the elements of the list are permutations
    **************************************)
 
@@ -361,14 +361,14 @@ apply permutation_length; auto.
 apply permutation_sym; apply split_one_permutation; auto.
 apply split_one_permutation; auto.
 Qed.
- 
+
 Theorem all_permutations_permutation :
  forall l1 l2 : list A, In l1 (all_permutations l2) -> permutation l1 l2.
 intros l1 l2 H; apply all_permutations_aux_permutation with (n := length l2);
  auto.
 Qed.
- 
-(************************************** 
+
+(**************************************
    A permutation is in the list
    **************************************)
 
@@ -399,17 +399,17 @@ apply permutation_inv with (a := a1).
 apply permutation_trans with (1 := H2).
 apply permutation_sym; apply split_one_permutation; auto.
 Qed.
- 
+
 Theorem permutation_all_permutations :
  forall l1 l2 : list A, permutation l1 l2 -> In l1 (all_permutations l2).
 intros l1 l2 H; unfold all_permutations in |- *;
  apply permutation_all_permutations_aux; auto.
 Qed.
 
-(************************************** 
+(**************************************
    Permutation is decidable
    **************************************)
- 
+
 Definition permutation_dec :
   (forall a b : A, {a = b} + {a <> b}) ->
   forall l1 l2 : list A, {permutation l1 l2} + {~ permutation l1 l2}.
@@ -418,10 +418,10 @@ case (In_dec (list_eq_dec H) l1 (all_permutations l2)).
 intros i; left; apply all_permutations_permutation; auto.
 intros i; right; contradict i; apply permutation_all_permutations; auto.
 Defined.
- 
+
 End permutation.
 
-(************************************** 
+(**************************************
    Hints
    **************************************)
 
@@ -430,7 +430,7 @@ Hint Resolve permutation_refl.
 Hint Resolve permutation_app_comp.
 Hint Resolve permutation_app_swap.
 
-(************************************** 
+(**************************************
    Implicits
    **************************************)
 
@@ -439,10 +439,10 @@ Implicit Arguments split_one [A].
 Implicit Arguments all_permutations [A].
 Implicit Arguments permutation_dec [A].
 
-(************************************** 
+(**************************************
    Permutation is compatible with map
    **************************************)
- 
+
 Theorem permutation_map :
  forall (A B : Set) (f : A -> B) l1 l2,
  permutation l1 l2 -> permutation (map f l1) (map f l2).
@@ -450,8 +450,8 @@ intros A B f l1 l2 H; elim H; simpl in |- *; auto.
 intros l0 l3 l4 H0 H1 H2 H3; apply permutation_trans with (2 := H3); auto.
 Qed.
 Hint Resolve permutation_map.
- 
-(************************************** 
+
+(**************************************
   Permutation  of a map can be inverted
   *************************************)
 
@@ -482,7 +482,7 @@ case H2 with (1 := HH2); auto.
 intros l5 (HH3, HH4); exists l5; split; auto.
 apply permutation_trans with (1 := HH3); auto.
 Qed.
- 
+
 Theorem permutation_map_ex :
  forall (A B : Set) (f : A -> B) l1 l2,
  permutation (map f l1) l2 ->
@@ -491,10 +491,10 @@ intros A0 B f l1 l2 H; apply permutation_map_ex_aux with (l1 := map f l1);
  auto.
 Qed.
 
-(************************************** 
+(**************************************
    Permutation is compatible with flat_map
  **************************************)
- 
+
 Theorem permutation_flat_map :
  forall (A B : Set) (f : A -> list B) l1 l2,
  permutation l1 l2 -> permutation (flat_map f l1) (flat_map f l2).
diff --git a/coqprime/Coqprime/Pmod.v b/coqprime/Coqprime/Pmod.v
index f64af48e3..3075b10f9 100644
--- a/coqprime/Coqprime/Pmod.v
+++ b/coqprime/Coqprime/Pmod.v
@@ -33,11 +33,11 @@ Fixpoint div_eucl (a b : positive) {struct a} : N * N :=
     let (q, r) := div_eucl a' b in
     match q, r with
     | N0, N0 => (0%N, 0%N)                 (* Impossible *)
-    | N0, Npos r =>  
+    | 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 => 
+    | Npos q, Npos r =>
       if (xI r) ?< b then (Npos (xO q), Npos (xI r))
       else (Npos (xI q),PminusN (xI r) b)
     end
@@ -46,17 +46,17 @@ Infix "/" := div_eucl : P_scope.
 
 Open Scope Z_scope.
 Opaque Zmult.
-Lemma div_eucl_spec : forall a b, 
+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). 
+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 ]] => 
+  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.
@@ -65,16 +65,16 @@ Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega).
   rewrite PminusN_le...
   generalize H1; zsimpl; auto.
   intros p H; rewrite H;
-  match goal with 
-  | [|- context [ ?xx ?< b ]] => 
+  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 ]] => 
+  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.
@@ -86,8 +86,8 @@ Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega).
    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 ]] => 
+  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.
@@ -98,8 +98,8 @@ Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega).
   intros p H; rewrite H; simpl; intros H1; split; auto.
   zsimpl; ring.
   intros p p1 H; rewrite H.
-  match goal with 
-  | [|- context [ ?xx ?< b ]] => 
+  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.
@@ -107,8 +107,8 @@ Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega).
   generalize H1; zsimpl; auto.
   rewrite PminusN_le...
   generalize H1; zsimpl; auto.
-  match goal with 
-  | [|- context [ ?xx ?< b ]] => 
+  match goal with
+  | [|- context [ ?xx ?< b ]] =>
     generalize (is_lt_spec xx b);destruct (xx ?< b)
   | _ => idtac
   end; zsimpl; simpl.
@@ -130,15 +130,15 @@ Fixpoint Pmod (a b : positive) {struct a} : N :=
     | N0 => 0%N
     | Npos r' =>
       if (xO r') ?< b then Npos (xO r')
-      else PminusN (xO r') b 
+      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' => 
+    | Npos r' =>
       if (xI r') ?< b then Npos (xI r')
-      else PminusN (xI r') b 
+      else PminusN (xI r') b
     end
   end.
 
@@ -151,8 +151,8 @@ Proof with auto.
  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 ]] => 
+  match goal with
+   | [|- context [ ?xx ?< b ]] =>
       assert (H2 := is_lt_spec xx b);destruct (xx ?< b)
   | _ => idtac
   end;simpl) ...
@@ -175,17 +175,17 @@ Proof.
  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 (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). 
+ 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.
@@ -197,7 +197,7 @@ 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.
 
@@ -205,7 +205,7 @@ 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). 
+ assert (0 <= fst (a / b) * b).
   destruct (fst (a / b));simpl;auto with zarith.
  auto with zarith.
 Qed.
@@ -236,7 +236,7 @@ Fixpoint gcd_log2 (a b c:positive) {struct c}: option positive :=
    end
  end.
 
-Fixpoint egcd_log2 (a b c:positive) {struct c}: 
+Fixpoint egcd_log2 (a b c:positive) {struct c}:
     option (Z * Z * positive) :=
  match a/b with
  |    (_, N0)  => Some (0, 1, b)
@@ -244,14 +244,14 @@ Fixpoint egcd_log2 (a b c:positive) {struct c}:
    match b/r, c with
    | (_, N0), _ => Some (1, -q, r)
    | (q', Npos r'), xH    => None
-   | (q', Npos r'), xO c' => 
+   | (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' => 
+   | (q', Npos r'), xI c' =>
         match egcd_log2 r r' c' with
           None => None
         | Some (u', v', w') =>
@@ -261,13 +261,13 @@ Fixpoint egcd_log2 (a b c:positive) {struct c}:
    end
  end.
 
-Lemma egcd_gcd_log2: forall c a b, 
+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 
+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;
@@ -276,27 +276,27 @@ induction c; simpl; auto; try
   intros ((p1,p2),p3); case gcd_log2; auto).
 Qed.
 
-Ltac rw l := 
+Ltac rw l :=
   match l with
    | (?r, ?r1) =>
        match type of r with
          True => rewrite <- r1
       |  _ => rw r; rw r1
-      end 
+      end
   | ?r => rewrite r
-  end. 
+  end.
 
-Lemma egcd_log2_ok: forall c a b, 
+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); 
+ 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; 
+  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;
@@ -305,11 +305,11 @@ induction c; simpl; auto;
 Qed.
 
 
-Fixpoint log2 (a:positive) : positive := 
- match a with 
+Fixpoint log2 (a:positive) : positive :=
+ match a with
  | xH => xH
- | xO a => Psucc (log2 a) 
- | xI a => Psucc (log2 a) 
+ | 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.
@@ -335,18 +335,18 @@ Proof.
  assert (H1:= Zlt_0_pos (log2 a));elimtype False;omega.
 Qed.
 
-Lemma mod_log2 : 
+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. 
+ 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 -> 
+  forall c a b, Zpos b <= Zpos a -> log2 b <= log2 c ->
    gcd_log2 a b c <> None.
 Proof.
  induction c;simpl;intros;
@@ -360,12 +360,12 @@ Proof.
   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 -> 
+   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;
@@ -386,8 +386,8 @@ Proof.
  intros a b c H1 H2; apply gcd_log2_Zle; trivial.
  apply gcd_log2_None; trivial.
 Qed.
- 
-Lemma gcd_log2_mod0 : 
+
+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.
 
@@ -405,7 +405,7 @@ Proof.
 Qed.
 
 Opaque Pmod.
-Lemma gcd_log2_mod : forall a b, Zpos b <= Zpos a -> 
+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).
@@ -426,7 +426,7 @@ Proof.
  rewrite mod1 in Hmod;discriminate Hmod.
 Qed.
 
-Lemma gcd_log2_xO_Zle : 
+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.
@@ -434,7 +434,7 @@ Proof.
  apply gcd_log2_None_aux;auto with zarith.
 Qed.
 
-Lemma gcd_log2_xO_Zlt : 
+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).
@@ -445,7 +445,7 @@ Proof.
  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. 
+ apply log2_Zle.
  replace (Zpos p) with (Z_of_N (Npos p));trivial.
  apply mod_le_a with a;trivial.
 Qed.
@@ -468,13 +468,13 @@ Qed.
 
 Definition gcd a b :=
   match gcd_log2 a b (xO b) with
-  | Some p => p 
+  | 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 
+  | Some p => p
   | None => (* can not appear *) (1,1,1%positive)
   end.
 
@@ -499,15 +499,15 @@ Proof.
  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. 
+ assert  (r <= b). omega.
  generalize (gcd_log2_None _ _ H2).
- destruct (gcd_log2 b r r);intros;trivial. 
+ 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. 
+ assert  (r <= b). omega.
  generalize (gcd_log2_None _ _ H3).
- destruct (gcd_log2 b r r);intros;trivial. 
+ destruct (gcd_log2 b r r);intros;trivial.
 Qed.
 
 Require Import ZArith.
@@ -515,7 +515,7 @@ Require Import Znumtheory.
 
 Hint Rewrite  Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc.
 
-Ltac mauto := 
+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).
@@ -534,13 +534,13 @@ Proof with mauto.
  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 
+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) 
+ 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);
@@ -548,7 +548,7 @@ Proof with mauto.
  intros; subst; split; try apply Zis_gcd_sym; auto.
 Qed.
 
-Definition Zgcd a b := 
+Definition Zgcd a b :=
   match a, b with
   | Z0, _ => b
   | _, Z0 => a
@@ -563,8 +563,8 @@ 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_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.
@@ -573,24 +573,24 @@ Proof.
  apply Zis_gcd_minus;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd.
 Qed.
 
-Definition Zegcd a b := 
+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 => 
+  | 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 => 
+  | Zpos a, Zpos b =>
      match egcd a b with (u,v,w) => (u,v, Zpos w) end
-  | Zneg a, Zneg b => 
+  | 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, 
+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.
@@ -604,11 +604,11 @@ Proof.
  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); 
+ 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; 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.
diff --git a/coqprime/Coqprime/Pocklington.v b/coqprime/Coqprime/Pocklington.v
index 9871cd3e6..09c0b901c 100644
--- a/coqprime/Coqprime/Pocklington.v
+++ b/coqprime/Coqprime/Pocklington.v
@@ -12,14 +12,14 @@ Require Import Tactic.
 Require Import ZCAux.
 Require Import Zp.
 Require Import FGroup.
-Require Import EGroup. 
+Require Import EGroup.
 Require Import Euler.
 
 Open Scope Z_scope.
 
-Theorem Pocklington: 
-forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> 
-   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
+Theorem Pocklington:
+forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 ->
+   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
   forall n, prime n -> (n | N) -> n mod F1 = 1.
 intros N F1 R1 HF1 HR1 Neq Rec n Hn H.
 assert (HN: 1 < N).
@@ -73,9 +73,9 @@ apply Zdivide_trans with (1:= HiF1); rewrite Neq; apply Zdivide_factor_r.
 apply Zorder_div; auto.
 Qed.
 
-Theorem PocklingtonCorollary1: 
+Theorem PocklingtonCorollary1:
 forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> N < F1 * F1 ->
-   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
+   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
    prime N.
 intros N F1 R1 H H1 H2 H3 H4; case (prime_dec N); intros H5; auto.
 assert (HN: 1 < N).
@@ -93,9 +93,9 @@ apply Pocklington with (R1 := R1) (4 := H4); auto.
 apply Zlt_square_mult_inv; auto with zarith.
 Qed.
 
-Theorem PocklingtonCorollary2: 
-forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> 
-   (forall p,  prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
+Theorem PocklingtonCorollary2:
+forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 ->
+   (forall p,  prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
   forall n, 0 <= n -> (n | N) -> n mod F1 = 1.
 intros N F1 R1 H1 H2 H3 H4 n H5; pattern n; apply prime_induction; auto.
 assert (HN: 1 < N).
@@ -114,9 +114,9 @@ Qed.
 
 Definition isSquare x := exists y, x = y * y.
 
-Theorem PocklingtonExtra: 
+Theorem PocklingtonExtra:
 forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 ->
-   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
+   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
    forall m, 1 <= m ->  (forall l, 1 <= l < m -> ~((l * F1 + 1) | N)) ->
     let s := (R1 / (2 * F1)) in
     let r := (R1 mod (2 * F1)) in
@@ -186,7 +186,7 @@ case (Zeven_odd_dec (c + d)); auto; intros O1.
 contradict ER1; apply Zeven_not_Zodd; rewrite L6; rewrite <- Zplus_assoc; apply Zeven_plus_Zeven; auto.
 apply Zeven_mult_Zeven_r; auto.
 assert (L6_2: Zeven (c * d)).
-case (Zeven_odd_dec c); intros HH1. 
+case (Zeven_odd_dec c); intros HH1.
 apply Zeven_mult_Zeven_l; auto.
 case (Zeven_odd_dec d); intros HH2.
 apply Zeven_mult_Zeven_r; auto.
@@ -237,9 +237,9 @@ rewrite <- L10.
 replace (8 * s) with (4 * (2 * s)); auto with zarith; try rewrite L11; ring.
 Qed.
 
-Theorem PocklingtonExtraCorollary: 
+Theorem PocklingtonExtraCorollary:
 forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 ->
-   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
+   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
     let s := (R1 / (2 * F1)) in
     let r := (R1 mod (2 * F1)) in
       N < 2 * F1 * F1 * F1 ->  (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N.
diff --git a/coqprime/Coqprime/PocklingtonCertificat.v b/coqprime/Coqprime/PocklingtonCertificat.v
index ecf4462ed..9d3a032fd 100644
--- a/coqprime/Coqprime/PocklingtonCertificat.v
+++ b/coqprime/Coqprime/PocklingtonCertificat.v
@@ -34,7 +34,7 @@ Definition nprim sc :=
  | Pock_certif n _ _ _ => n
  | SPock_certif n _ _ => n
  | Ell_certif n _ _ _ _ _ _ => n
- 
+
  end.
 
 Open Scope positive_scope.
@@ -51,11 +51,11 @@ Definition mkProd' (l:dec_prime) :=
   fold_right (fun (k:positive*positive) r => times (fst k) r) 1%positive l.
 
 Definition mkProd_pred (l:dec_prime) :=
-  fold_right (fun (k:positive*positive) r => 
+  fold_right (fun (k:positive*positive) r =>
     if ((snd k) ?= 1)%P then r else times (pow (fst k) (Ppred (snd k))) r)
   1%positive l.
 
-Definition mkProd (l:dec_prime) := 
+Definition mkProd (l:dec_prime) :=
   fold_right (fun (k:positive*positive) r => times (pow (fst k) (snd k)) r) 1%positive l.
 
 (* [pow_mod a m n] return [a^m mod n] *)
@@ -84,7 +84,7 @@ Definition Npow_mod a m n :=
 
 (* [fold_pow_mod a [q1,_;...;qn,_]] b = a ^(q1*...*qn) mod b *)
 (* invariant a mod N = a *)
-Definition fold_pow_mod a l n := 
+Definition fold_pow_mod a l n :=
   fold_left
     (fun a' (qp:positive*positive) =>  Npow_mod a' (fst qp) n)
     l a.
@@ -99,15 +99,15 @@ Definition times_mod x y n :=
 Definition Npred_mod p n :=
   match p with
   | N0 => Npos (Ppred n)
-  | Npos p => 
+  | Npos p =>
       if (p ?= 1) then N0
       else Npos (Ppred p)
-   end.     
- 
+   end.
+
 Fixpoint all_pow_mod (prod a : N) (l:dec_prime) (n:positive) {struct l}: N*N :=
   match l with
   | nil => (prod,a)
-  | (q,_) :: l => 
+  | (q,_) :: l =>
     let m := Npred_mod (fold_pow_mod a l n) n in
     all_pow_mod (times_mod prod m n) (Npow_mod a q n) l n
   end.
@@ -117,19 +117,19 @@ Fixpoint pow_mod_pred (a:N) (l:dec_prime) (n:positive) {struct l} : N :=
   | nil => a
   | (q,p)::l =>
     if (p ?= 1) then pow_mod_pred a l n
-    else 
+    else
       let a' := iter_pos _ (fun x => Npow_mod x q n) a (Ppred p) in
       pow_mod_pred a' l n
   end.
 
 Definition is_odd p :=
-  match p with 
+  match p with
   | xO _ => false
   | _     => true
   end.
 
-Definition is_even p := 
-   match p with 
+Definition is_even p :=
+   match p with
   | xO _ => true
   | _       => false
   end.
@@ -137,19 +137,19 @@ Definition is_even p :=
 Definition check_s_r s r sqrt :=
  match s with
  | N0 => true
- | Npos p => 
+ | Npos p =>
     match (Zminus (square r) (xO (xO (xO p)))) with
     | Zpos x =>
        let sqrt2 := square sqrt in
        let sqrt12 := square (Psucc sqrt)  in
-       if sqrt2 ?< x then x ?< sqrt12 
+       if sqrt2 ?< x then x ?< sqrt12
        else false
     | Zneg _ => true
     | Z0 => false
     end
   end.
 
-Definition test_pock N a dec sqrt := 
+Definition test_pock N a dec sqrt :=
   if (2 ?< N) then
     let Nm1 := Ppred N in
     let F1 := mkProd dec in
@@ -165,8 +165,8 @@ Definition test_pock N a dec sqrt :=
               match all_pow_mod 1%N A dec N with
               | (Npos p, Npos aNm1) =>
                 if (aNm1 ?= 1) then
-                  if gcd p N ?= 1 then 
-                    if check_s_r s r sqrt then 
+                  if gcd p N ?= 1 then
+                    if check_s_r s r sqrt then
 		      (N ?< (times ((times ((xO F1)+r+1) F1) + r) F1) + 1)
                     else false
                   else false
@@ -176,10 +176,10 @@ Definition test_pock N a dec sqrt :=
             | _ => false
             end
 	  else false
-        else false 
+        else false
       else false
     | _=> false
-    end      
+    end
   else false.
 
 Fixpoint is_in (p : positive) (lc : Certif) {struct lc} : bool :=
@@ -191,10 +191,10 @@ Fixpoint is_in (p : positive) (lc : Certif) {struct lc} : bool :=
 Fixpoint all_in (lc : Certif) (lp : dec_prime) {struct lp} : bool :=
   match lp with
   | nil => true
-  | (p,_) :: lp => 
-    if all_in lc lp 
+  | (p,_) :: lp =>
+    if all_in lc lp
     then is_in p lc
-    else false 
+    else false
   end.
 
 Definition gt2 n :=
@@ -212,7 +212,7 @@ Fixpoint test_Certif (lc : Certif) : bool :=
      if gt2 p then
        match Mp p with
        | Zpos n' =>
-          if (n ?= n') then 
+          if (n ?= n') then
             match SS p with
             | Z0 => true
             | _ => false
@@ -220,10 +220,10 @@ Fixpoint test_Certif (lc : Certif) : bool :=
           else false
       | _ => false
       end
-    else false 
+    else false
     else false
   | (Pock_certif n a dec sqrt) :: lc =>
-    if test_pock n a dec sqrt then 
+    if test_pock n a dec sqrt then
      if all_in lc dec then test_Certif lc else false
     else false
 (* Shoudl be done later to do it with Z *)
@@ -231,9 +231,9 @@ Fixpoint test_Certif (lc : Certif) : bool :=
   | (Ell_certif _ _ _ _ _ _ _):: lc => false
   end.
 
-Lemma pos_eq_1_spec : 
+Lemma pos_eq_1_spec :
   forall p,
-    if (p ?= 1)%P then p = xH 
+    if (p ?= 1)%P then p = xH
     else (1 < p).
 Proof.
  unfold Zlt;destruct p;simpl; auto; red;reflexivity.
@@ -248,7 +248,7 @@ Lemma mod_unique : forall b q1 r1 q2 r2,
 Proof with auto with zarith.
  intros b q1 r1 q2 r2 H1 H2 H3.
  assert (r2 = (b * q1 + r1) -b*q2).  rewrite H3;ring.
- assert (b*(q2 - q1) = r1 - r2 ).  rewrite H;ring. 
+ assert (b*(q2 - q1) = r1 - r2 ).  rewrite H;ring.
  assert (-b < r1 - r2 < b). omega.
  destruct (Ztrichotomy q1 q2) as [H5 | [H5 | H5]].
   assert (q2 - q1 >= 1).  omega.
@@ -277,10 +277,10 @@ Qed.
 
 Hint Resolve Zpower_gt_0 Zlt_0_pos Zge_0_pos Zlt_le_weak Zge_0_pos_add: zmisc.
 
-Hint Rewrite  Zpos_mult Zpower_mult Zpower_1_r Zmod_mod Zpower_exp 
+Hint Rewrite  Zpos_mult Zpower_mult Zpower_1_r Zmod_mod Zpower_exp
             times_Zmult square_Zmult Psucc_Zplus: zmisc.
 
-Ltac mauto := 
+Ltac mauto :=
   trivial;autorewrite with zmisc;trivial;auto with zmisc zarith.
 
 Lemma mod_lt : forall a (b:positive), a mod b < b.
@@ -318,9 +318,9 @@ Proof.
  assert (b>0). mauto.
  unfold Zmod; assert (H1 := Z_div_mod a b H).
  destruct (Zdiv_eucl a b) as (q2, r2).
- assert (H2 := div_eucl_spec a b). 
+ assert (H2 := div_eucl_spec a b).
  assert (Z_of_N (fst (a / b)%P) = q2 /\ Z_of_N (snd (a/b)%P) = r2).
- destruct H1;destruct H2. 
+ destruct H1;destruct H2.
  apply mod_unique with b;mauto.
  split;mauto.
  unfold Zle;destruct (snd (a / b)%P);intro;discriminate.
@@ -351,7 +351,7 @@ Proof.
  destruct (pow_mod a m n); mauto.
  rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc.
  rewrite <- IHm. destruct (pow_mod a m n);simpl; mauto.
-Qed. 
+Qed.
 Hint Rewrite pow_mod_spec Zpower_0 : zmisc.
 
 Lemma Npow_mod_spec : forall a p n, Z_of_N (Npow_mod a p n) = a^p mod n.
@@ -360,7 +360,7 @@ Proof.
 Qed.
 Hint Rewrite Npow_mod_spec : zmisc.
 
-Lemma iter_Npow_mod_spec : forall n q p a, 
+Lemma iter_Npow_mod_spec : forall n q p a,
   Z_of_N (iter_pos N (fun x : N => Npow_mod x q n) a p) = a^q^p mod n.
 Proof.
  induction p; mauto; intros; simpl Pos.iter; mauto; repeat rewrite IHp.
@@ -370,28 +370,28 @@ Proof.
 Qed.
 Hint Rewrite iter_Npow_mod_spec : zmisc.
 
-Lemma fold_pow_mod_spec : forall (n:positive) l (a:N), 
+Lemma fold_pow_mod_spec : forall (n:positive) l (a:N),
   Z_of_N a = a mod n ->
-  Z_of_N (fold_pow_mod a l n) = a^(mkProd' l) mod n. 
+  Z_of_N (fold_pow_mod a l n) = a^(mkProd' l) mod n.
 Proof.
- unfold fold_pow_mod;induction l; simpl fold_left; simpl mkProd'; 
+ unfold fold_pow_mod;induction l; simpl fold_left; simpl mkProd';
   intros; mauto.
  rewrite IHl; mauto.
 Qed.
-Hint Rewrite fold_pow_mod_spec : zmisc.				
+Hint Rewrite fold_pow_mod_spec : zmisc.
 
 Lemma pow_mod_pred_spec : forall (n:positive) l (a:N),
   Z_of_N a = a mod n ->
-  Z_of_N (pow_mod_pred a l n) = a^(mkProd_pred l) mod n. 
+  Z_of_N (pow_mod_pred a l n) = a^(mkProd_pred l) mod n.
 Proof.
  unfold pow_mod_pred;induction l;simpl mkProd;intros; mauto.
  destruct a as (q,p).
  simpl mkProd_pred.
  destruct (p ?= 1)%P; rewrite IHl; mauto; simpl.
 Qed.
-Hint Rewrite pow_mod_pred_spec : zmisc.				
+Hint Rewrite pow_mod_pred_spec : zmisc.
 
-Lemma mkProd_pred_mkProd : forall l, 
+Lemma mkProd_pred_mkProd : forall l,
    (mkProd_pred l)*(mkProd' l) = mkProd l.
 Proof.
  induction l;simpl;intros; mauto.
@@ -418,7 +418,7 @@ Proof.
   assert ( 0 <= a mod b < b).
    apply Z_mod_lt; mauto.
   destruct (mod_unique b (a/b) (a mod b) 0 a H0 H); mauto.
-  rewrite <- Z_div_mod_eq; mauto. 
+  rewrite <- Z_div_mod_eq; mauto.
 Qed.
 
 Lemma Npred_mod_spec : forall p n, Z_of_N p < Zpos n ->
@@ -455,7 +455,7 @@ Qed.
 Lemma fold_aux : forall a N (n:positive) l prod,
   fold_left
      (fun (r : Z) (k : positive * positive) =>
-      r * (a ^(N / fst k) - 1) mod n) l (prod mod n) mod n = 
+      r * (a ^(N / fst k) - 1) mod n) l (prod mod n) mod n =
   fold_left
      (fun (r : Z) (k : positive * positive) =>
       r * (a^(N / fst k) - 1)) l prod mod n.
@@ -465,12 +465,12 @@ Qed.
 
 Lemma fst_all_pow_mod :
  forall (n a:positive) l  (R:positive) (prod A :N),
-  1 < n -> 
+  1 < n ->
   Z_of_N prod = prod mod n ->
   Z_of_N A = a^R mod n ->
-  Z_of_N (fst (all_pow_mod prod A l n)) = 
+  Z_of_N (fst (all_pow_mod prod A l n)) =
     (fold_left
-      (fun r (k:positive*positive) => 
+      (fun r (k:positive*positive) =>
         (r * (a ^ (R* mkProd' l / (fst k)) - 1))) l prod) mod n.
 Proof.
  induction l;simpl;intros; mauto.
@@ -483,23 +483,23 @@ Proof.
  rewrite Z_div_mult;auto with zmisc zarith.
  rewrite <- fold_aux.
  rewrite <- (fold_aux a (R * q * mkProd' l) n l (prod * (a ^ (R * mkProd' l) - 1)))...
- assert ( ((prod * (A ^ mkProd' l - 1)) mod n) = 
+ assert ( ((prod * (A ^ mkProd' l - 1)) mod n) =
               ((prod * ((a ^ R) ^ mkProd' l - 1)) mod n)).
   repeat rewrite (Zmult_mod prod);auto with zmisc.
   rewrite Zminus_mod;auto with zmisc.
   rewrite (Zminus_mod ((a ^ R) ^ mkProd' l));auto with zmisc.
   rewrite (Zpower_mod (a^R));auto with zmisc.  rewrite H1; mauto.
- rewrite H3; mauto. 
+ rewrite H3; mauto.
  rewrite H1; mauto.
 Qed.
 
 Lemma is_odd_Zodd : forall p, is_odd p = true -> Zodd p.
-Proof. 
+Proof.
  destruct p;intros;simpl;trivial;discriminate.
 Qed.
 
 Lemma is_even_Zeven : forall p, is_even p = true -> Zeven p.
-Proof. 
+Proof.
  destruct p;intros;simpl;trivial;discriminate.
 Qed.
 
@@ -513,12 +513,12 @@ Qed.
 Lemma le_square : forall x y, 0 <= x  -> x <= y -> x*x <= y*y.
 Proof.
  intros; apply Zle_trans with (x*y).
- apply Zmult_le_compat_l;trivial. 
+ apply Zmult_le_compat_l;trivial.
  apply Zmult_le_compat_r;trivial. omega.
 Qed.
 
-Lemma borned_square : forall x y, 0 <= x -> 0 <= y -> 
-                             x*x < y*y < (x+1)*(x+1) -> False. 
+Lemma borned_square : forall x y, 0 <= x -> 0 <= y ->
+                             x*x < y*y < (x+1)*(x+1) -> False.
 Proof.
  intros;destruct (Z_lt_ge_dec x y) as [z|z].
  assert (x + 1 <= y). omega.
@@ -539,25 +539,25 @@ Qed.
 Ltac spec_dec :=
  repeat match goal with
  | [H:(?x ?= ?y)%P = _ |- _] =>
-      generalize (is_eq_spec x y); 
+      generalize (is_eq_spec x y);
       rewrite H;clear H; autorewrite with zmisc;
       intro
   | [H:(?x ?< ?y)%P = _ |- _] =>
-      generalize (is_lt_spec x y); 
+      generalize (is_lt_spec x y);
       rewrite H; clear H; autorewrite with zmisc;
       intro
   end.
 
 Ltac elimif :=
  match goal with
- | [H: (if ?b then _ else _) = _ |- _] => 
+ | [H: (if ?b then _ else _) = _ |- _] =>
       let H1 := fresh "H" in
       (CaseEq b;intros H1; rewrite H1 in H;
       try discriminate H); elimif
  | _ => spec_dec
  end.
 
-Lemma check_s_r_correct : forall s r sqrt, check_s_r s r sqrt = true -> 
+Lemma check_s_r_correct : forall s r sqrt, check_s_r s r sqrt = true ->
           Z_of_N s = 0 \/ ~ isSquare (r * r - 8 * s).
 Proof.
  unfold check_s_r;intros.
@@ -566,7 +566,7 @@ Proof.
    rewrite H1 in H;try discriminate H.
  elimif.
  assert (Zpos (xO (xO (xO s))) = 8 * s).  repeat rewrite Zpos_xO_add;ring.
- generalizeclear H1; rewrite H2;mauto;intros. 
+ generalizeclear H1; rewrite H2;mauto;intros.
  apply (not_square sqrt).
  simpl Z.of_N; rewrite H1;auto.
  intros (y,Heq).
@@ -579,10 +579,10 @@ Proof.
  destruct y;discriminate Heq2.
 Qed.
 
-Lemma in_mkProd_prime_div_in : 
-  forall p:positive,  prime p -> 
-  forall (l:dec_prime),   
-    (forall k, In k l -> prime (fst k)) -> 
+Lemma in_mkProd_prime_div_in :
+  forall p:positive,  prime p ->
+  forall (l:dec_prime),
+    (forall k, In k l -> prime (fst k)) ->
     Zdivide p (mkProd l) -> exists n,In (p, n) l.
 Proof.
  induction l;simpl mkProd; simpl In; mauto.
@@ -591,7 +591,7 @@ Proof.
  apply Zdivide_le; auto with zarith.
  intros.
  case prime_mult with (2 := H1); auto with zarith; intros H2.
- exists (snd a);left. 
+ exists (snd a);left.
  destruct a;simpl in *.
  assert (Zpos p = Zpos p0).
    rewrite (prime_div_Zpower_prime p1 p p0); mauto.
@@ -616,7 +616,7 @@ Proof.
  rewrite Zmult_comm;apply Zis_gcd_for_euclid2;simpl in *.
  apply Zis_gcd_sym;auto.
 Qed.
- 
+
 Lemma test_pock_correct : forall N a dec sqrt,
    (forall k, In k dec -> prime (Zpos (fst k))) ->
    test_pock N a dec sqrt = true ->
@@ -632,10 +632,10 @@ Proof.
  generalize (div_eucl_spec R1 (xO (mkProd dec)));
  destruct ((R1 / xO (mkProd dec))%P) as (s,r'); mauto;intros (H7,H8).
  destruct r' as [|r];try discriminate H0.
- generalize (fst_all_pow_mod N a dec (R1*mkProd_pred dec) 1 
+ generalize (fst_all_pow_mod N a dec (R1*mkProd_pred dec) 1
          (pow_mod_pred (pow_mod a R1 N) dec N)).
  generalize (snd_all_pow_mod N dec 1 (pow_mod_pred (pow_mod a R1 N) dec N)).
- destruct (all_pow_mod 1 (pow_mod_pred (pow_mod a R1 N) dec N) dec N) as 
+ destruct (all_pow_mod 1 (pow_mod_pred (pow_mod a R1 N) dec N) dec N) as
   (prod,aNm1); mauto; simpl Z_of_N.
  destruct prod as [|prod];try discriminate H0.
  destruct aNm1 as [|aNm1];try discriminate H0;elimif.
@@ -654,7 +654,7 @@ Proof.
  end; mauto.
  rewrite Zmod_small; mauto.
  assert (1 < mkProd dec).
-  assert (H14 := Zlt_0_pos (mkProd dec)). 
+  assert (H14 := Zlt_0_pos (mkProd dec)).
   assert (1 <= mkProd dec); mauto.
   destruct (Zle_lt_or_eq _ _ H15); mauto.
   inversion H16. rewrite <- H18 in H5;discriminate H5.
@@ -671,7 +671,7 @@ Proof.
   auto with zmisc zarith.
  rewrite H2; mauto.
  apply is_even_Zeven; auto.
- apply is_odd_Zodd; auto. 
+ apply is_odd_Zodd; auto.
  intros p; case p; clear p.
  intros HH; contradict HH.
  apply not_prime_0.
@@ -691,7 +691,7 @@ Proof.
  revert H2; mauto; intro H2.
  rewrite <- H2.
  match goal with |- context [fold_left ?f _ _] =>
-   apply (ListAux.fold_left_invol_in _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) 
+   apply (ListAux.fold_left_invol_in _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k))
      with (b := (p, q)); auto with zarith
  end.
  rewrite <- Heqr.
@@ -702,7 +702,7 @@ Proof.
  apply check_s_r_correct with sqrt; mauto.
 Qed.
 
-Lemma is_in_In : 
+Lemma is_in_In :
   forall p lc, is_in p lc = true -> exists c, In c lc /\ p = nprim c.
 Proof.
  induction lc;simpl;try (intros;discriminate).
@@ -711,7 +711,7 @@ Proof.
  destruct (IHlc H) as [c [H1 H2]];exists c;auto.
 Qed.
 
-Lemma all_in_In : 
+Lemma all_in_In :
  forall lc lp, all_in lc lp = true ->
  forall pq, In pq lp -> exists c, In c lc /\ fst pq = nprim c.
 Proof.
@@ -721,8 +721,8 @@ Proof.
  rewrite <- H0;simpl;apply is_in_In;trivial.
 Qed.
 
-Lemma test_Certif_In_Prime : 
-  forall lc, test_Certif lc = true -> 
+Lemma test_Certif_In_Prime :
+  forall lc, test_Certif lc = true ->
    forall c, In c lc -> prime (nprim c).
 Proof with mauto.
  induction lc;simpl;intros. elim H0.
@@ -732,10 +732,10 @@ Proof with mauto.
  CaseEq (Mp p);[intros Heq|intros N' Heq|intros N' Heq];rewrite Heq in H;
   try discriminate H. elimif.
  CaseEq (SS p);[intros Heq'|intros N'' Heq'|intros N'' Heq'];rewrite Heq' in H;
-  try discriminate H. 
+  try discriminate H.
  rewrite H2;rewrite <- Heq.
 apply LucasLehmer;trivial.
-(destruct p; try discriminate H1). 
+(destruct p; try discriminate H1).
 simpl in H1; generalize (is_lt_spec 2 p); rewrite H1; auto.
 elimif.
 apply (test_pock_correct N a d p); mauto.
@@ -748,9 +748,8 @@ discriminate.
 discriminate.
 Qed.
 
-Lemma Pocklington_refl : 
+Lemma Pocklington_refl :
   forall c lc, test_Certif (c::lc) = true -> prime (nprim c).
 Proof.
  intros c lc Heq;apply test_Certif_In_Prime with (c::lc);trivial;simpl;auto.
 Qed.
-
diff --git a/coqprime/Coqprime/Root.v b/coqprime/Coqprime/Root.v
index 2f65790d6..0b432b788 100644
--- a/coqprime/Coqprime/Root.v
+++ b/coqprime/Coqprime/Root.v
@@ -7,9 +7,9 @@
 (*************************************************************)
 
 (***********************************************************************
-      Root.v                                                                                       
-                                                                                                         
-      Proof that a polynomial has at most n roots                                 
+      Root.v
+
+      Proof that a polynomial has at most n roots
 ************************************************************************)
 Require Import ZArith.
 Require Import List.
@@ -30,11 +30,11 @@ Variable zero one: A.
 
 Let pol := list A.
 
-Definition toA z := 
-match z with 
-  Z0  => zero 
-| Zpos p => iter_pos _ (plus one) zero p 
-| Zneg p => op (iter_pos _ (plus one) zero p) 
+Definition toA z :=
+match z with
+  Z0  => zero
+| Zpos p => iter_pos _ (plus one) zero p
+| Zneg p => op (iter_pos _ (plus one) zero p)
 end.
 
 Fixpoint eval (p: pol) (x: A) {struct p} : A :=
@@ -47,8 +47,8 @@ Fixpoint div (p: pol) (x: A) {struct p} : pol * A :=
 match p with
   nil => (nil, zero)
 | a::nil => (nil, a)
-| a::p1 => 
-                     (snd (div p1 x)::fst (div p1 x), 
+| a::p1 =>
+                     (snd (div p1 x)::fst (div p1 x),
                      (plus a (mult  x (snd (div p1 x)))))
 end.
 
@@ -82,7 +82,7 @@ simpl; intuition.
 intros a2 p2 Rec Hi; split.
 case Rec; auto with datatypes.
 intros H H1 i.
-replace (In i (fst (div (a1 :: a2 :: p2) a))) with 
+replace (In i (fst (div (a1 :: a2 :: p2) a))) with
  (snd (div (a2::p2) a) = i \/  In i (fst (div (a2::p2) a))); auto.
 intros [Hi1 | Hi1]; auto.
 rewrite <- Hi1; auto.
@@ -93,13 +93,13 @@ case Rec; auto with datatypes.
 Qed.
 
 
-Theorem div_correct: 
+Theorem div_correct:
   forall p x y, P x -> P y -> (forall i, In i p -> P i) -> eval p y = plus (mult (eval (fst (div p x)) y) (plus y (op x))) (snd (div p x)).
 intros p x y; elim p; simpl.
 intros; rewrite mult_zero; try rewrite plus_zero; auto.
 intros a l; case l; simpl; auto.
 intros _ px py pa; rewrite (fun x => mult_comm x zero); repeat rewrite mult_zero; try apply plus_comm; auto.
-intros a1 l1. 
+intros a1 l1.
 generalize (div_P (a1::l1) x); simpl.
 match goal with |-  context[fst ?A]   => case A end; simpl.
 intros q r Hd Rec px py pi.
@@ -117,7 +117,7 @@ repeat rewrite mult_plus_distr; auto.
 repeat (rewrite (fun x y => (mult_comm (plus x y))) || rewrite mult_plus_distr); auto.
 rewrite (fun x => (plus_comm  x (mult y r))); auto.
 repeat rewrite  plus_assoc; try apply f_equal2 with (f := plus); auto.
-2: repeat rewrite mult_assoc; try rewrite (fun y => mult_comm y (op x)); 
+2: repeat rewrite mult_assoc; try rewrite (fun y => mult_comm y (op x));
     repeat rewrite mult_assoc; auto.
 rewrite (fun z => (plus_comm  z (mult (op x) r))); auto.
 repeat rewrite  plus_assoc; try apply f_equal2 with (f := plus); auto.
@@ -127,7 +127,7 @@ rewrite (plus_comm (op x)); try rewrite plus_op_zero; auto.
 rewrite (fun x => mult_comm x zero); try rewrite mult_zero; try rewrite plus_zero; auto.
 Qed.
 
-Theorem div_correct_factor: 
+Theorem div_correct_factor:
   forall p a, (forall i, In i p -> P i) -> P a ->
        eval p a = zero -> forall x,  P x -> eval p x =  (mult (eval (fst (div p a)) x) (plus x (op a))).
 intros p a Hp Ha H x px.
@@ -143,14 +143,14 @@ Theorem length_decrease: forall p x, p <> nil -> (length (fst (div p x)) < lengt
 intros p x; elim p; simpl; auto.
 intros H1; case H1; auto.
 intros a l; case l; simpl; auto.
-intros a1 l1. 
+intros a1 l1.
 match goal with |-  context[fst ?A]   => case A end; simpl; auto with zarith.
 intros p1 _ H H1.
 apply lt_n_S; apply H; intros; discriminate.
 Qed.
 
-Theorem root_max: 
-forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) -> 
+Theorem root_max:
+forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) ->
   (forall x, In x l -> eval p x = zero) -> (length p <= length l)%nat -> forall x, P x -> eval p x = zero.
 intros p l; generalize p; elim l; clear l p; simpl; auto.
 intros p; case p; simpl; auto.
@@ -178,8 +178,8 @@ apply lt_n_Sm_le;apply lt_le_trans with (length (a1 :: p2)); auto with zarith.
 apply length_decrease; auto with datatypes.
 Qed.
 
-Theorem root_max_is_zero: 
-forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) -> 
+Theorem root_max_is_zero:
+forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) ->
   (forall x, In x l -> eval p x = zero) -> (length p <= length l)%nat -> forall x, (In x p) -> x = zero.
 intros p l; generalize p; elim l; clear l p; simpl; auto.
 intros p; case p; simpl; auto.
@@ -236,4 +236,4 @@ apply sym_equal; apply plus_zero; auto.
 intros HH; case Hz; rewrite <- HH; auto.
 Qed.
 
-End Root.
\ No newline at end of file
+End Root.
diff --git a/coqprime/Coqprime/Tactic.v b/coqprime/Coqprime/Tactic.v
index 93a244149..b0f8f4f28 100644
--- a/coqprime/Coqprime/Tactic.v
+++ b/coqprime/Coqprime/Tactic.v
@@ -8,19 +8,19 @@
 
 
 (**********************************************************************
-       Tactic.v                                                                                    
-          Useful tactics                                                                       
+       Tactic.v
+          Useful tactics
  **********************************************************************)
 
 (**************************************
-  A simple tactic to end a proof 
+  A simple tactic to end a proof
 **************************************)
 Ltac  finish := intros; auto; trivial; discriminate.
 
 
 (**************************************
  A tactic for proof by contradiction
-     with contradict H 
+     with contradict H
          H: ~A |-   B      gives           |-   A
          H: ~A |- ~ B     gives  H: B |-   A
          H:   A |-   B      gives           |- ~ A
@@ -28,19 +28,19 @@ Ltac  finish := intros; auto; trivial; discriminate.
          H:   A |- ~ B     gives  H: A |- ~ A
 **************************************)
 
-Ltac  contradict name := 
+Ltac  contradict name :=
      let term := type of name in (
-     match term with 
-       (~_) => 
-          match goal with 
+     match term with
+       (~_) =>
+          match goal with
             |- ~ _  => let x := fresh in
-                     (intros x; case name; 
+                     (intros x; case name;
                       generalize x; clear x name;
                       intro name)
           | |- _    => case name; clear name
           end
-     | _ => 
-          match goal with 
+     | _ =>
+          match goal with
             |- ~ _  => let x := fresh in
                     (intros x;  absurd term;
                        [idtac | exact name]; generalize x; clear x name;
@@ -60,10 +60,10 @@ Ltac case_eq name :=
 
 
 (**************************************
- A tactic to use f_equal? theorems 
+ A tactic to use f_equal? theorems
 **************************************)
 
-Ltac eq_tac := 
+Ltac eq_tac :=
  match goal with
       |-  (?g _ = ?g _) => apply f_equal with (f := g)
  |     |-  (?g ?X _ = ?g  ?X _) => apply f_equal with (f := g X)
@@ -77,7 +77,7 @@ Ltac eq_tac :=
  |     |-  (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g)
  end.
 
-(************************************** 
+(**************************************
  A stupid tactic that tries auto also after applying sym_equal
 **************************************)
 
diff --git a/coqprime/Coqprime/UList.v b/coqprime/Coqprime/UList.v
index 7b9d982ea..7dbd8562d 100644
--- a/coqprime/Coqprime/UList.v
+++ b/coqprime/Coqprime/UList.v
@@ -7,33 +7,33 @@
 (*************************************************************)
 
 (***********************************************************************
-      UList.v                                                                                       
-                                                                                                         
-      Definition of list with distinct elements                                 
-                                                                                                         
-      Definition: ulist                                                                         
+      UList.v
+
+      Definition of list with distinct elements
+
+      Definition: ulist
 ************************************************************************)
 Require Import List.
 Require Import Arith.
 Require Import Permutation.
 Require Import ListSet.
- 
+
 Section UniqueList.
 Variable A : Set.
 Variable eqA_dec : forall (a b : A),  ({ a = b }) + ({ a <> b }).
 (* A list is unique if there is not twice the same element in the list *)
- 
+
 Inductive ulist : list A ->  Prop :=
   ulist_nil: ulist nil
  | ulist_cons: forall a l, ~ In a l -> ulist l ->  ulist (a :: l) .
 Hint Constructors ulist .
 (* Inversion theorem *)
- 
+
 Theorem ulist_inv: forall a l, ulist (a :: l) ->  ulist l.
 intros a l H; inversion H; auto.
 Qed.
 (* The append of two unique list is unique if the list are distinct *)
- 
+
 Theorem ulist_app:
  forall l1 l2,
  ulist l1 ->
@@ -48,7 +48,7 @@ apply ulist_inv with ( 1 := H0 ); auto.
 intros a0 H3 H4; apply (H2 a0); auto.
 Qed.
 (* Iinversion theorem the appended list *)
- 
+
 Theorem ulist_app_inv:
  forall l1 l2 (a : A), ulist (l1 ++ l2) -> In a l1 -> In a l2 ->  False.
 intros l1; elim l1; simpl; auto.
@@ -59,7 +59,7 @@ apply (H l2 a0); auto.
 apply ulist_inv with ( 1 := H0 ); auto.
 Qed.
 (* Iinversion theorem the appended list *)
- 
+
 Theorem ulist_app_inv_l: forall (l1 l2 : list A), ulist (l1 ++ l2) ->  ulist l1.
 intros l1; elim l1; simpl; auto.
 intros a l H l2 H0.
@@ -68,13 +68,13 @@ intros H5; case iH2; auto with datatypes.
 apply H with l2; auto.
 Qed.
 (* Iinversion theorem the appended list *)
- 
+
 Theorem ulist_app_inv_r: forall (l1 l2 : list A), ulist (l1 ++ l2) ->  ulist l2.
 intros l1; elim l1; simpl; auto.
 intros a l H l2 H0; inversion H0; auto.
 Qed.
 (* Uniqueness is decidable *)
- 
+
 Definition ulist_dec: forall l,  ({ ulist l }) + ({ ~ ulist l }).
 intros l; elim l; auto.
 intros a l1 [H|H]; auto.
@@ -83,7 +83,7 @@ right; red; intros H1; inversion H1; auto.
 right; intros H1; case H; apply ulist_inv with ( 1 := H1 ).
 Defined.
 (* Uniqueness is compatible with permutation *)
- 
+
 Theorem ulist_perm:
  forall (l1 l2 : list A), permutation l1 l2 -> ulist l1 ->  ulist l2.
 intros l1 l2 H; elim H; clear H l1 l2; simpl; auto.
@@ -103,7 +103,7 @@ intros H; case iH1; simpl; auto.
 inversion_clear H0 as [|ia il iH1 iH2]; auto.
 inversion iH2; auto.
 Qed.
- 
+
 Theorem ulist_def:
  forall l a,
  In a l -> ulist l ->  ~ (exists l1 , permutation l (a :: (a :: l1)) ).
@@ -112,7 +112,7 @@ absurd (ulist (a :: (a :: l1))); auto.
 intros H2; inversion_clear H2; simpl; auto with datatypes.
 apply ulist_perm with ( 1 := H1 ); auto.
 Qed.
- 
+
 Theorem ulist_incl_permutation:
  forall (l1 l2 : list A),
  ulist l1 -> incl l1 l2 ->  (exists l3 , permutation l2 (l1 ++ l3) ).
@@ -134,7 +134,7 @@ intros l4 H4; exists l4.
 apply permutation_trans with (a :: l3); auto.
 apply permutation_sym; auto.
 Qed.
- 
+
 Theorem ulist_eq_permutation:
  forall (l1 l2 : list A),
  ulist l1 -> incl l1 l2 -> length l1 = length l2 ->  permutation l1 l2.
@@ -150,7 +150,7 @@ replace l1 with (app l1 l3); auto.
 apply permutation_sym; auto.
 rewrite H5; rewrite app_nil_end; auto.
 Qed.
- 
+
 
 Theorem ulist_incl_length:
  forall (l1 l2 : list A), ulist l1 -> incl l1 l2 ->  le (length l1) (length l2).
@@ -166,8 +166,8 @@ intros l1 l2 H1 H2 H3 H4.
 apply ulist_eq_permutation; auto.
 apply le_antisym; apply ulist_incl_length; auto.
 Qed.
- 
- 
+
+
 Theorem ulist_incl_length_strict:
  forall (l1 l2 : list A),
  ulist l1 -> incl l1 l2 -> ~ incl l2 l1 ->  lt (length l1) (length l2).
@@ -180,14 +180,14 @@ intros H2; case Hi0; auto.
 intros a HH; apply permutation_in with ( 1 := H2 ); auto.
 intros a l Hl0; (rewrite plus_comm; simpl; rewrite plus_comm; auto with arith).
 Qed.
- 
+
 Theorem in_inv_dec:
  forall (a b : A) l, In a (cons b l) ->  a = b \/ ~ a = b /\ In a l.
 intros a b l H; case (eqA_dec a b); auto; intros H1.
 right; split; auto; inversion H; auto.
 case H1; auto.
 Qed.
- 
+
 Theorem in_ex_app_first:
  forall (a : A) (l : list A),
  In a l ->
@@ -203,7 +203,7 @@ case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl;
 subst; auto.
 intros H4; case H4; auto.
 Qed.
- 
+
 Theorem ulist_inv_ulist:
  forall (l : list A),
  ~ ulist l ->
@@ -239,7 +239,7 @@ replace (l1 ++ (a1 :: (l2 ++ (a1 :: l3))))
      with ((l1 ++ (a1 :: l2)) ++ (a1 :: l3)); auto with datatypes.
 (repeat (rewrite <- ass_app; simpl)); auto.
 Qed.
- 
+
 Theorem incl_length_repetition:
  forall (l1 l2 : list A),
  incl l1 l2 ->
@@ -253,11 +253,11 @@ intros l1 l2 H H0; apply ulist_inv_ulist.
 intros H1; absurd (le (length l1) (length l2)); auto with arith.
 apply ulist_incl_length; auto.
 Qed.
- 
+
 End UniqueList.
 Implicit Arguments ulist [A].
 Hint Constructors ulist .
- 
+
 Theorem ulist_map:
  forall (A B : Set) (f : A ->  B) l,
  (forall x y, (In x l) -> (In y l) ->  f x = f y ->  x = y) -> ulist l ->  ulist (map f l).
@@ -270,7 +270,7 @@ case in_map_inv with ( 1 := H1 ); auto with datatypes.
 intros b1 [Hb1 Hb2].
 replace a1 with b1; auto with datatypes.
 Qed.
- 
+
 Theorem ulist_list_prod:
  forall (A : Set) (l1 l2 : list A),
  ulist l1 -> ulist l2 ->  ulist (list_prod l1 l2).
diff --git a/coqprime/Coqprime/ZCAux.v b/coqprime/Coqprime/ZCAux.v
index de03a2fe2..2da30c800 100644
--- a/coqprime/Coqprime/ZCAux.v
+++ b/coqprime/Coqprime/ZCAux.v
@@ -7,9 +7,9 @@
 (*************************************************************)
 
 (**********************************************************************
-     ZCAux.v                                                                                           
-                                                                                                          
-     Auxillary functions & Theorems                                              
+     ZCAux.v
+
+     Auxillary functions & Theorems
  **********************************************************************)
 
 Require Import ArithRing.
@@ -57,7 +57,7 @@ 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. 
+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.
@@ -94,13 +94,13 @@ ring.
 exists 0; repeat split; try rewrite Zpower_1_r; try rewrite Zpower_exp_0; auto with zarith.
 Qed.
 
-Theorem prime_div_induction: 
+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. 
+    (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.
@@ -119,7 +119,7 @@ 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. 
+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.
@@ -256,7 +256,7 @@ 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; 
+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.
 
@@ -278,13 +278,13 @@ 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. 
+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. 
+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.
diff --git a/coqprime/Coqprime/ZCmisc.v b/coqprime/Coqprime/ZCmisc.v
index c1bdacc63..67709a146 100644
--- a/coqprime/Coqprime/ZCmisc.v
+++ b/coqprime/Coqprime/ZCmisc.v
@@ -27,14 +27,14 @@ 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 
+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, 
+
+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.
@@ -48,17 +48,17 @@ 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, 
+Lemma Pminus_mask_spec :
+   forall p q,
     match Pminus_mask p q with
     | IsNul    => Zpos p =  Zpos q
-    | IsPos k => Zpos p = q + k 
+    | 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)]] => 
+  match goal with
+  | [|- context [(Pminus_mask ?p1 ?q1)]] =>
     assert (H1 := IHp q1);destruct (Pminus_mask p1 q1)
   | _ => idtac
   end;simpl ...
@@ -69,7 +69,7 @@ Proof with zsimpl;auto with zarith.
  assert (H:= Zlt_0_pos q) ...   assert (H:= Zlt_0_pos q) ...
 Qed.
 
-Definition PminusN x y := 
+Definition PminusN x y :=
   match Pminus_mask x y with
   | IsPos k => Npos k
   | _ => N0
@@ -100,7 +100,7 @@ Definition is_lt (n m : positive) :=
   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. 
+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.
@@ -113,7 +113,7 @@ Definition is_eq a b :=
   | _ => 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.
 
@@ -123,14 +123,14 @@ Proof.
 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. 
+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. 
+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.
@@ -145,8 +145,8 @@ Definition is_Eq 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. 
+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.
diff --git a/coqprime/Coqprime/ZProgression.v b/coqprime/Coqprime/ZProgression.v
index 51ce91cdc..ec69df5a6 100644
--- a/coqprime/Coqprime/ZProgression.v
+++ b/coqprime/Coqprime/ZProgression.v
@@ -10,7 +10,7 @@ Require Export Iterator.
 Require Import ZArith.
 Require Export UList.
 Open Scope Z_scope.
- 
+
 Theorem next_n_Z: forall n m,  next_n Zsucc n m = n + Z_of_nat m.
 intros n m; generalize n; elim m; clear n m.
 intros n; simpl; auto with zarith.
@@ -19,7 +19,7 @@ replace (n + Z_of_nat (S m)) with (Zsucc n + Z_of_nat m); auto with zarith.
 rewrite <- H; auto with zarith.
 rewrite inj_S; auto with zarith.
 Qed.
- 
+
 Theorem Zprogression_end:
  forall n m,
   progression Zsucc n (S m) =
@@ -33,7 +33,7 @@ replace (Zsucc n1 + Z_of_nat m1) with (n1 + Z_of_nat (S m1)); auto with zarith.
 replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1); auto with zarith.
 rewrite inj_S; auto with zarith.
 Qed.
- 
+
 Theorem Zprogression_pred_end:
  forall n m,
   progression Zpred n (S m) =
@@ -47,7 +47,7 @@ replace (Zpred n1 - Z_of_nat m1) with (n1 - Z_of_nat (S m1)); auto with zarith.
 replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1); auto with zarith.
 rewrite inj_S; auto with zarith.
 Qed.
- 
+
 Theorem Zprogression_opp:
  forall n m,
   rev (progression Zsucc n m) = progression Zpred (n + Z_of_nat (pred m)) m.
@@ -63,7 +63,7 @@ intros m1;
  replace (n + Z_of_nat (pred (S m1))) with (Zpred (n + Z_of_nat (S m1))); auto.
 rewrite inj_S; simpl; (unfold Zpred; unfold Zsucc); auto with zarith.
 Qed.
- 
+
 Theorem Zprogression_le_init:
  forall n m p, In p (progression Zsucc n m) ->  (n <= p).
 intros n m; generalize n; elim m; clear n m; simpl; auto.
@@ -71,7 +71,7 @@ intros; contradiction.
 intros m H n p [H1|H1]; auto with zarith.
 generalize (H _ _ H1); auto with zarith.
 Qed.
- 
+
 Theorem Zprogression_le_end:
  forall n m p, In p (progression Zsucc n m) ->  (p < n + Z_of_nat m).
 intros n m; generalize n; elim m; clear n m; auto.
@@ -84,14 +84,14 @@ apply Zplus_lt_compat_l; red; simpl; auto with zarith.
 apply Zlt_le_trans with (Zsucc n + Z_of_nat m); auto with zarith.
 rewrite inj_S; rewrite Zplus_succ_comm; auto with zarith.
 Qed.
- 
+
 Theorem ulist_Zprogression: forall a n,  ulist (progression Zsucc a n).
 intros a n; generalize a; elim n; clear a n; simpl; auto with zarith.
 intros n H1 a; apply ulist_cons; auto.
 intros H2; absurd (Zsucc a <= a); auto with zarith.
 apply Zprogression_le_init with ( 1 := H2 ).
 Qed.
- 
+
 Theorem in_Zprogression:
  forall a b n, ( a <= b < a + Z_of_nat n ) ->  In b (progression Zsucc a n).
 intros a b n; generalize a b; elim n; clear a b n; auto with zarith.
diff --git a/coqprime/Coqprime/ZSum.v b/coqprime/Coqprime/ZSum.v
index 3a7f14065..95a8f74a5 100644
--- a/coqprime/Coqprime/ZSum.v
+++ b/coqprime/Coqprime/ZSum.v
@@ -19,14 +19,14 @@ 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.
@@ -39,7 +39,7 @@ 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);
@@ -85,7 +85,7 @@ 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.
@@ -128,20 +128,20 @@ 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.
@@ -191,13 +191,13 @@ Lemma Zsum_add:
 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 ->
@@ -241,7 +241,7 @@ 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.
@@ -256,7 +256,7 @@ 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 ->
@@ -266,7 +266,7 @@ Theorem Zsum_Zsum_f:
 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)) =
@@ -274,7 +274,7 @@ Theorem Zsum_com:
 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 ->
@@ -301,7 +301,7 @@ 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) ->
@@ -327,7 +327,7 @@ 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.
diff --git a/coqprime/Coqprime/Zp.v b/coqprime/Coqprime/Zp.v
index 1e5295191..6383b08b9 100644
--- a/coqprime/Coqprime/Zp.v
+++ b/coqprime/Coqprime/Zp.v
@@ -7,12 +7,12 @@
 (*************************************************************)
 
 (**********************************************************************
-    Zp.v                        
-                                                                     
+    Zp.v
+
     Build the group of the inversible element on {1, 2, .., n-1}
     for the multiplication modulo n
-                                                                 
-    Definition: ZpGroup              
+
+    Definition: ZpGroup
  **********************************************************************)
 Require Import ZArith Znumtheory Zpow_facts.
 Require Import Tactic.
@@ -34,14 +34,14 @@ Variable n: Z.
 Hypothesis n_pos: 1 < n.
 
 
-(************************************** 
+(**************************************
   mkZp m creates {m, m - 1, ..., 0}
  **************************************)
 
 Fixpoint mkZp_aux (m: nat): list Z:=
-  Z_of_nat m :: match m with O => nil | (S m1) => mkZp_aux m1 end. 
+  Z_of_nat m :: match m with O => nil | (S m1) => mkZp_aux m1 end.
 
-(************************************** 
+(**************************************
   Some properties of mkZp_aux
  **************************************)
 
@@ -75,13 +75,13 @@ rewrite inj_S; intros H1.
 case in_mkZp_aux with (1 := H1); auto with zarith.
 Qed.
 
-(************************************** 
+(**************************************
   mkZp creates {n - 1, ..., 1, 0}
  **************************************)
 
 Definition mkZp := mkZp_aux (Zabs_nat (n - 1)).
 
-(************************************** 
+(**************************************
   Some properties of mkZp
  **************************************)
 
@@ -109,13 +109,13 @@ Theorem mkZp_ulist: ulist mkZp.
 unfold mkZp; apply mkZp_aux_ulist; auto.
 Qed.
 
-(************************************** 
+(**************************************
   Multiplication of two pairs
  **************************************)
 
 Definition pmult (p q: Z) := (p * q) mod n.
 
-(************************************** 
+(**************************************
   Properties of multiplication
  **************************************)
 
@@ -155,7 +155,7 @@ Qed.
 
 Definition Lrel := isupport_aux _ pmult  mkZp 1 Z_eq_dec (progression Zsucc 0 (Zabs_nat n)).
 
-Theorem rel_prime_is_inv: 
+Theorem rel_prime_is_inv:
   forall a, is_inv Z pmult mkZp 1 Z_eq_dec a = if (rel_prime_dec a n) then true else false.
 assert (Hu: 0 < n); try apply Zlt_trans with 1; auto with zarith.
 intros a; case (rel_prime_dec a n); intros H.
@@ -184,8 +184,8 @@ unfold pmult in H2; rewrite (Zmult_comm c); try rewrite H2.
 ring.
 Qed.
 
-(************************************** 
-   We are now ready to build our group 
+(**************************************
+   We are now ready to build our group
  **************************************)
 
 Definition ZPGroup : (FGroup pmult).
@@ -232,7 +232,7 @@ intros a H; unfold ZPGroup; simpl.
 apply isupport_is_in.
 unfold Lrel in H; apply  isupport_aux_is_inv_true with (1 := H).
 apply mkZp_in; auto.
-assert (In a (progression Zsucc 0 (Zabs_nat  n))). 
+assert (In a (progression Zsucc 0 (Zabs_nat  n))).
 apply  (isupport_aux_incl _ pmult mkZp 1 Z_eq_dec); auto.
 split.
 apply Zprogression_le_init with (1 := H0).
@@ -246,7 +246,7 @@ simpl in H; apply  isupport_is_inv_true with (1 := H).
 apply in_Zprogression.
 rewrite Zplus_0_l; rewrite inj_Zabs_nat; auto with zarith.
 rewrite Zabs_eq; auto with zarith.
-assert (In a mkZp). 
+assert (In a mkZp).
 apply  (isupport_aux_incl _ pmult mkZp 1 Z_eq_dec); auto.
 apply in_mkZp; auto.
 Qed.
@@ -330,8 +330,8 @@ apply Z_mod_lt; auto with zarith.
 Qed.
 
 
-Theorem Zpower_mod_is_gpow: 
-  forall p q n (Hn: 1 < n), rel_prime p n -> 0 <= q -> p ^ q mod n = gpow (p mod n) (ZPGroup n Hn) q. 
+Theorem Zpower_mod_is_gpow:
+  forall p q n (Hn: 1 < n), rel_prime p n -> 0 <= q -> p ^ q mod n = gpow (p mod n) (ZPGroup n Hn) q.
 intros p q n H Hp H1; generalize H1; pattern q; apply natlike_ind; simpl; auto.
 intros _; apply Zmod_small; auto with zarith.
 intros n1 Hn1 Rec _; simpl.
@@ -343,7 +343,7 @@ rewrite Zmult_mod; auto.
 Qed.
 
 
-Theorem Zorder_div_power: forall p q n, 1 < n -> rel_prime p n -> p ^ q  mod n = 1 -> (Zorder p n | q). 
+Theorem Zorder_div_power: forall p q n, 1 < n -> rel_prime p n -> p ^ q  mod n = 1 -> (Zorder p n | q).
 intros p q n H H1 H2.
 assert (Hq: 0 <= q).
 generalize H2; case q; simpl; auto with zarith.
@@ -355,7 +355,7 @@ apply in_mod_ZPGroup; auto.
 rewrite <- Zpower_mod_is_gpow; auto with zarith.
 Qed.
 
-Theorem Zorder_div:  forall p n,  prime n -> ~(n | p) -> (Zorder p n | n - 1). 
+Theorem Zorder_div:  forall p n,  prime n -> ~(n | p) -> (Zorder p n | n - 1).
 intros p n H; unfold Zorder.
 case (Z_le_dec n 1); intros H1 H2.
 contradict H1; generalize (prime_ge_2 n H); auto with zarith.
diff --git a/coqprime/Makefile b/coqprime/Makefile
index c8e44a658..2b995982e 100644
--- a/coqprime/Makefile
+++ b/coqprime/Makefile
@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject -o Makefile 
+# coq_makefile -f _CoqProject -o Makefile
 #
 
 .DEFAULT_GOAL := all
@@ -151,7 +151,7 @@ endif
 #                                     #
 #######################################
 
-all: $(VOFILES) 
+all: $(VOFILES)
 
 quick: $(VOFILES:.vo=.vio)
 
@@ -316,4 +316,3 @@ $(addsuffix .beautified,$(VFILES)): %.v.beautified:
 # Edit at your own risks !
 #
 # END OF WARNING
-