Strip trailing whitespace

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

56 files changed, 641 insertions, 645 deletions

diff --git a/LICENSE b/LICENSE
index 191fe6c04..d2edc96ea 100644
--- a/LICENSE
+++ b/LICENSE
@@ -19,4 +19,3 @@ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.
-
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
-
diff --git a/crypto-defects.md b/crypto-defects.md
index 28a0a8c25..55761db3f 100644
--- a/crypto-defects.md
+++ b/crypto-defects.md
@@ -20,9 +20,9 @@ appearing in our code.
 | [ic#237002094](https://github.com/mit-plv/fiat-crypto/pull/42#issuecomment-237002094) | Barrett reduction for p256 | 1 conditional subtraction instead of 2 | unkown if ok |
 | [openssl#1593](https://rt.openssl.org/Ticket/Display.html?id=1593&user=guest&pass=guest) | P384 modular reduction | carry handling | [exploitable](https://eprint.iacr.org/2011/633.pdf) |
 | [go#fa09811d](https://github.com/golang/crypto/commit/84e98f45760e87786b7f24603b8166a6fa09811d) | poly1305 reduction | AMD64 asm, missing subtraction of 3 | found quickly |
-| [jose-adobe](https://blogs.adobe.com/security/2017/03/critical-vulnerability-uncovered-in-json-encryption.html) | ECDH-ES | 5 libraries | not onCurve | 
-| [tweetnacl-m\[15\]](http://seb.dbzteam.org/blog/2014/04/28/tweetnacl_arithmetic_bug.html) | GF(2^255-19) freeze | bit-twiddly C | bounds? typo? | 
-| [tweetnacl-U32](https://web.archive.org/web/20160305001036/http://blog.skylable.com/2014/05/tweetnacl-carrybit-bug/) | irrelevant | bit-twiddly C | `sizeof(long)!=32` | 
+| [jose-adobe](https://blogs.adobe.com/security/2017/03/critical-vulnerability-uncovered-in-json-encryption.html) | ECDH-ES | 5 libraries | not onCurve |
+| [tweetnacl-m\[15\]](http://seb.dbzteam.org/blog/2014/04/28/tweetnacl_arithmetic_bug.html) | GF(2^255-19) freeze | bit-twiddly C | bounds? typo? |
+| [tweetnacl-U32](https://web.archive.org/web/20160305001036/http://blog.skylable.com/2014/05/tweetnacl-carrybit-bug/) | irrelevant | bit-twiddly C | `sizeof(long)!=32` |
 | [CVE-2017-3732](https://www.openssl.org/news/secadv/20170126.txt) | x^2 mod m | Montgomery form, AMD64 assembly | [carry](https://boringssl.googlesource.com/boringssl/+/d103616db14ca9587f074efaf9f09a48b8ca80cb%5E%21/), exploitable |
 | [openssl#c2633b8f](https://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=b62b2454fadfccaf5e055a1810d72174c2633b8f;ds=sidebyside) | a + b mod p256 |  Montgomery form, AMD64 assembly | [non-canonical](https://mta.openssl.org/pipermail/openssl-dev/2016-August/008179.html) |
 | [openssl#59dfcabf](https://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=e3057a57caf4274ea1fb074518e4714059dfcabf;ds=sidebyside) | Weier. affine <-> Jacobian |  Montgomery form, AMD64 and C | ∞ confusion |
diff --git a/expansion.md b/expansion.md
index 15e3b7e3d..ca74dfcdc 100644
--- a/expansion.md
+++ b/expansion.md
@@ -70,7 +70,7 @@ involve register allocation and instruction scheduling.
 
 **loops** for our PHOAS language. Possibly hardcoded to [fold_left] of [seq], or
 something else that is sufficient to encode C "for" loops. Importantly, we
-should have a way to reify existing code 
+should have a way to reify existing code
 
 **modules** for our PHOAS language so we don't have to inline everything.
 Basically we want to allow one Coq-level object to represent a collection of
diff --git a/optimizations.md b/optimizations.md
index 90c0bc4e7..ca26adc5e 100644
--- a/optimizations.md
+++ b/optimizations.md
@@ -1,13 +1,13 @@
-| Category              |  Name                               |  Status           |  Lemma(s)                                                                                                                                                                                                                                  |  Description                                                                                                                                                                                                                                     | 
-|-----------------------|-------------------------------------|-------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| 
-| Field Arithmetic      |  Unsaturated limbs/delayed carrying |  Implemented      |  [ModularBaseSystemProofs.v#L347](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/ModularBaseSystemProofs.v#L347)                                                                                                 |  Represent field elements using more machine words than strictly necessary in order to delay carrying (for example, represent a 255-bit number using 51 bits per 64-bit word)                                                                    | 
-| Field Arithmetic      |  Division-free Modular Reduction    |  Implemented      |  [PseudoMersenneBaseParamProofs.v#L41](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v#L41)                                                                                       |  Reduce $x$ modulo $2^k-c$ by splitting $x$ into $a$ and $b$ such that $a + 2^k * b = x$, then returning $a + c * b$                                                                                                                             | 
-| Field Arithmetic      |  Inverse square root                |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Compute $\frac{1}{\sqrt{x}}$ rather than $\sqrt{x}$. Then, for example, in order to compute $\sqrt{\frac{x}{y}}$, compute $x * \frac{1}{\sqrt{xy}}$ rather than doing two expensive square root computations                                    | 
-| Field Arithmetic      |  Addition Chain Exponentiation      |  Implemented      |  [AdditionChainExponentiation.v#L53](https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/AdditionChainExponentiation.v#L53)                                                                                                        |  https://en.wikipedia.org/wiki/Addition-chain_exponentiation                                                                                                                                                                                     | 
-| Field Arithmetic      |  Specialized Squaring               |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Write a specialized function for squaring field elts rather than just using mul                                                                                                                                                                 | 
-| Field Arithmetic      |  Karatsuba                          |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Use Karatsuba's trick for multiplication (mostly relevant for primes $> 400$ bits in size)                                                                                                                                                      | 
-| Elliptic Curve Points |  Extended Coordinates               |  Implemented      |  [ExtendedCoordinates.v#L258](https://github.com/mit-plv/fiat-crypto/blob/master/src/CompleteEdwardsCurve/ExtendedCoordinates.v#L258)                                                                                                      |  http://hyperelliptic.org/EFD/g1p/auto-edwards.html                                                                                                                                                                                              | 
-| Elliptic Curve Points |  Precomputed Tables                 |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Precompute powers of base point                                                                                                                                                                                                                 | 
-| Elliptic Curve Points |  Hex Exponentiation                 |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Use hexadecimal exponentiation for elliptic curve scalar multiplication                                                                                                                                                                         | 
-| Elliptic Curve Points |  Point Compression                  |  Implemented      |  [PointEncodingPre.v#L313](https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/PointEncodingPre.v#L313) and [PointEncodingPre.v#L412](https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/PointEncodingPre.v#L412) |  Instead of transmitting $(x,y)$ to transmit a point, transmit $y$ and a bit representing the sign of $x$. Decode $x$ by solving the curve equation for $x^2$, taking the square root, and picking the square root with the appropriate sign bit | 
-| Low-Level             |  Use Varied-size Registers          |  Half-Implemented |  [MapCastWithCastOp.v#L116](https://github.com/mit-plv/fiat-crypto/blob/master/src/Reflection/MapCastWithCastOp.v#L116)                                                                                                                    |  Rather than using the largest available integer size (e.g., `uint32_t` on x86_32, `uint64_t` on x86_64) for all operations, pick the smallest integer size which is guaranteed to fit the result for each arithmetic operation separately       | 
+| Category              |  Name                               |  Status           |  Lemma(s)                                                                                                                                                                                                                                  |  Description                                                                                                                                                                                                                                     |
+|-----------------------|-------------------------------------|-------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
+| Field Arithmetic      |  Unsaturated limbs/delayed carrying |  Implemented      |  [ModularBaseSystemProofs.v#L347](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/ModularBaseSystemProofs.v#L347)                                                                                                 |  Represent field elements using more machine words than strictly necessary in order to delay carrying (for example, represent a 255-bit number using 51 bits per 64-bit word)                                                                    |
+| Field Arithmetic      |  Division-free Modular Reduction    |  Implemented      |  [PseudoMersenneBaseParamProofs.v#L41](https://github.com/mit-plv/fiat-crypto/blob/master/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v#L41)                                                                                       |  Reduce $x$ modulo $2^k-c$ by splitting $x$ into $a$ and $b$ such that $a + 2^k * b = x$, then returning $a + c * b$                                                                                                                             |
+| Field Arithmetic      |  Inverse square root                |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Compute $\frac{1}{\sqrt{x}}$ rather than $\sqrt{x}$. Then, for example, in order to compute $\sqrt{\frac{x}{y}}$, compute $x * \frac{1}{\sqrt{xy}}$ rather than doing two expensive square root computations                                    |
+| Field Arithmetic      |  Addition Chain Exponentiation      |  Implemented      |  [AdditionChainExponentiation.v#L53](https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/AdditionChainExponentiation.v#L53)                                                                                                        |  https://en.wikipedia.org/wiki/Addition-chain_exponentiation                                                                                                                                                                                     |
+| Field Arithmetic      |  Specialized Squaring               |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Write a specialized function for squaring field elts rather than just using mul                                                                                                                                                                 |
+| Field Arithmetic      |  Karatsuba                          |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Use Karatsuba's trick for multiplication (mostly relevant for primes $> 400$ bits in size)                                                                                                                                                      |
+| Elliptic Curve Points |  Extended Coordinates               |  Implemented      |  [ExtendedCoordinates.v#L258](https://github.com/mit-plv/fiat-crypto/blob/master/src/CompleteEdwardsCurve/ExtendedCoordinates.v#L258)                                                                                                      |  http://hyperelliptic.org/EFD/g1p/auto-edwards.html                                                                                                                                                                                              |
+| Elliptic Curve Points |  Precomputed Tables                 |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Precompute powers of base point                                                                                                                                                                                                                 |
+| Elliptic Curve Points |  Hex Exponentiation                 |  Not Implemented  |  n/a                                                                                                                                                                                                                                       |  Use hexadecimal exponentiation for elliptic curve scalar multiplication                                                                                                                                                                         |
+| Elliptic Curve Points |  Point Compression                  |  Implemented      |  [PointEncodingPre.v#L313](https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/PointEncodingPre.v#L313) and [PointEncodingPre.v#L412](https://github.com/mit-plv/fiat-crypto/blob/master/src/Encoding/PointEncodingPre.v#L412) |  Instead of transmitting $(x,y)$ to transmit a point, transmit $y$ and a bit representing the sign of $x$. Decode $x$ by solving the curve equation for $x^2$, taking the square root, and picking the square root with the appropriate sign bit |
+| Low-Level             |  Use Varied-size Registers          |  Half-Implemented |  [MapCastWithCastOp.v#L116](https://github.com/mit-plv/fiat-crypto/blob/master/src/Reflection/MapCastWithCastOp.v#L116)                                                                                                                    |  Rather than using the largest available integer size (e.g., `uint32_t` on x86_32, `uint64_t` on x86_64) for all operations, pick the smallest integer size which is guaranteed to fit the result for each arithmetic operation separately       |
diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v
index 59ca72c6b..149a6373e 100644
--- a/src/Algebra/Field_test.v
+++ b/src/Algebra/Field_test.v
@@ -92,4 +92,4 @@ Module _fsatz_test.
       : x7 = x9 /\ y7 = y9.
     Proof using Type*. fsatz_prepare_hyps; split; fsatz. Qed.
   End _test.
-End _fsatz_test.
\ No newline at end of file
+End _fsatz_test.
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index 27c45dcec..01325de3f 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -196,4 +196,4 @@ Section CommutativeGroupByIsomorphism.
            | _ => solve [ eauto ]
            end.
   Qed.
-End CommutativeGroupByIsomorphism.
\ No newline at end of file
+End CommutativeGroupByIsomorphism.
diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v
index f52fc93ee..034ed4d4c 100644
--- a/src/Algebra/ScalarMult.v
+++ b/src/Algebra/ScalarMult.v
@@ -89,4 +89,4 @@ End ScalarMultHomomorphism.
 
 Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero}
   : @is_scalarmult G eq add zero (@scalarmult_ref G add zero).
-Proof. split; try exact _; intros; reflexivity. Qed.
\ No newline at end of file
+Proof. split; try exact _; intros; reflexivity. Qed.
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index b86ac09b9..d61ff5ba4 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -837,7 +837,7 @@ Module B.
 
     Section Select.
       Context {weight : nat -> Z}.
-      
+
       Definition select_cps {n} (mask cond:Z) (p:tuple Z n)
                  {T} (f:tuple Z n->T) :=
         dlet t := Z.zselect cond 0 mask in Tuple.map_cps (runtime_and t) p f.
diff --git a/src/Arithmetic/ModularArithmeticPre.v b/src/Arithmetic/ModularArithmeticPre.v
index b27ffd16d..3063d3a51 100644
--- a/src/Arithmetic/ModularArithmeticPre.v
+++ b/src/Arithmetic/ModularArithmeticPre.v
@@ -136,4 +136,4 @@ Next Obligation.
   replace (Z.succ (m - 2)) with (m-1) by omega.
   rewrite (Zmod_small 1) by omega.
   apply (fermat_little m Hm a Ha).
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v
index 990aa9dc8..8f9277f35 100644
--- a/src/Arithmetic/ModularArithmeticTheorems.v
+++ b/src/Arithmetic/ModularArithmeticTheorems.v
@@ -17,10 +17,10 @@ Module F.
     lazy iota beta delta [F.add F.sub F.mul F.opp F.to_Z F.of_Z proj1_sig] in *;
     try apply eqsig_eq;
     pull_Zmod.
-  
+
   (* FIXME: remove the pose proof once [monoid] no longer contains decidable equality *)
   Global Instance eq_dec {m} : DecidableRel (@eq (F m)). pose proof dec_eq_Z. exact _. Defined.
-  
+
   Global Instance commutative_ring_modulo m
     : @Algebra.Hierarchy.commutative_ring (F m) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul.
   Proof.
@@ -48,14 +48,14 @@ Module F.
     Lemma eq_of_Z_iff : forall x y : Z, x mod m = y mod m <-> F.of_Z m x = F.of_Z m y.
     Proof using Type. split; unwrap_F; congruence. Qed.
 
-    
+
     Lemma to_Z_of_Z : forall z, F.to_Z (F.of_Z m z) = z mod m.
     Proof using Type. unwrap_F; trivial. Qed.
 
     Lemma of_Z_to_Z x : F.of_Z m (F.to_Z x) = x :> F m.
     Proof using Type. unwrap_F; congruence. Qed.
 
-    
+
     Lemma of_Z_mod : forall x, F.of_Z m x = F.of_Z m (x mod m).
     Proof using Type. unwrap_F; trivial. Qed.
 
@@ -95,7 +95,7 @@ Module F.
     Lemma to_Z_mul : forall x y : F m,
         F.to_Z (x * y) = ((F.to_Z x * F.to_Z y) mod m)%Z.
     Proof using Type. unwrap_F; trivial. Qed.
-    
+
     Lemma of_Z_sub x y : F.of_Z _ (x - y) = F.of_Z _ x - F.of_Z _ y :> F m.
     Proof using Type. unwrap_F. trivial. Qed.
 
diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v
index c253752c5..edab4e065 100644
--- a/src/Arithmetic/PrimeFieldTheorems.v
+++ b/src/Arithmetic/PrimeFieldTheorems.v
@@ -95,7 +95,7 @@ Module F.
       rewrite <-H in q_3mod4; discriminate.
     Qed.
     Local Hint Resolve two_lt_q_3mod4.
-    
+
     Lemma sqrt_3mod4_correct (x:F q) :
       ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x)%F.
     Proof using Type*.
@@ -130,7 +130,7 @@ Module F.
                            constants [F.is_constant],
                            div (F.morph_div_theory q),
                            power_tac (F.power_theory q) [F.is_pow_constant]).
-    
+
     (* Any nonsquare element raised to (q-1)/4 (real implementations use 2 ^ ((q-1)/4) )
        would work for sqrt_minus1 *)
     Context (sqrt_minus1 : F q) (sqrt_minus1_valid : sqrt_minus1 * sqrt_minus1 = F.opp 1).
@@ -241,7 +241,7 @@ Module F.
   Module Iso.
     Section IsomorphicRings.
       Context {q:positive} {prime_q:prime q} {two_lt_q:2 < Z.pos q}.
-      Context 
+      Context
         {H : Type} {eq : H -> H -> Prop} {zero one : H}
         {opp : H -> H} {add sub mul : H -> H -> H}
         {phi : F q -> H} {phi' : H -> F q}
@@ -256,7 +256,7 @@ Module F.
         {pow_is_scalarmult:ScalarMult.is_scalarmult(G:=H)(eq:=eq)(add:=mul)(zero:=one)(mul:=fun (n:nat) (k:H) => pow k (NtoP (N.of_nat n)))}.
       Definition inv (x:H) := pow x (NtoP (Z.to_N (q - 2)%Z)).
       Definition div x y := mul (inv y) x.
-      
+
       Lemma ring :
         @Algebra.Hierarchy.ring H eq zero one opp add sub mul
         /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index 650cd7bcf..a66c268b0 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -49,14 +49,14 @@ a [tuple Z n] as output. This operation is called "compact".
 As an example, let's compact the product of 571 and 645 in base 10.
 At first, the partial products look like this:
 
-      
-                   1*6         
+
+                   1*6
             1*4    7*4     7*6
      1*5    7*5    5*5     5*4      5*6
     ------------------------------------
        1     10    100    1000    10000
-                   
-                     6         
+
+                     6
               4     28      42
        5     35     25      20       30
     ------------------------------------
@@ -75,7 +75,7 @@ bit. We add a 0 to the next column and continue.
      {carry_acc = 0; output=(5,)}
      STEP [4,35] (4 + 35 = 39)
      {carry_acc = 3; output=(9,5)}
-     
+
 This time, we have a carry. We add it to the third column and process
 that:
 
@@ -93,7 +93,7 @@ columns:
      {carry_acc = 4; output=(8,9,5)}
      STEP [4,20] (4 + 20 = 24)
      {carry_acc = 6; output=(4,8,9,5)}
-     
+
      STEP [6,30] (6 + 30 = 36)
      {carry_acc = 3; output=(6,4,8,9,5)}
 
@@ -213,7 +213,7 @@ Module Columns.
                | _ => progress (autorewrite with uncps push_id cancel_pair in * )
                | _ => progress break_match; try discriminate
                | _ => reflexivity
-               | _ => f_equal; ring 
+               | _ => f_equal; ring
                end.
     Qed. Hint Rewrite compact_digit_mod : div_mod.
 
@@ -229,9 +229,9 @@ Module Columns.
                | _ => progress (autorewrite with uncps push_id cancel_pair in * )
                | _ => progress break_match; try discriminate
                | _ => reflexivity
-               | _ => f_equal; ring 
+               | _ => f_equal; ring
                end.
-      assert (weight (S i) / weight i <> 0) by auto using Z.positive_is_nonzero. 
+      assert (weight (S i) / weight i <> 0) by auto using Z.positive_is_nonzero.
       match goal with |- _ = (?a + ?X) / ?D =>
                       transitivity  ((a + X mod D + D * (X / D)) / D);
                         [| rewrite (Z.div_mod'' X D) at 3; f_equal; auto; ring]
@@ -279,7 +279,7 @@ Module Columns.
         with (fun i s a => compact_digit i (s :: a)).
 
       apply mapi_with'_linvariant; [|tauto].
-      
+
       clear n inp. intros until 0. intros Hst Hys [Hmod Hdiv].
       pose proof (weight_positive n). pose proof (weight_divides n).
       autorewrite with push_basesystem_eval.
@@ -292,8 +292,8 @@ Module Columns.
                | _ => rewrite map_left_append
                | _ => rewrite B.Positional.eval_left_append
                | _ => rewrite weight_0, ?Z.div_1_r, ?Z.mod_1_r
-               | _ => rewrite Hdiv 
-               | _ => rewrite Hmod 
+               | _ => rewrite Hdiv
+               | _ => rewrite Hmod
                | _ => progress subst
                | _ => progress autorewrite with natsimplify cancel_pair push_basesystem_eval
                | _ => solve [split; ring_simplify; f_equal; ring]
@@ -424,7 +424,7 @@ Module Columns.
         (fun nq => B.Positional.to_associational_cps weight nq
         (fun Q => from_associational_cps weight n (P++Q)
         (fun R => compact_cps (div:=div) (modulo:=modulo) (add_get_carry:=add_get_carry) weight R f)))).
-   
+
     End Wrappers.
 End Columns.
 Hint Unfold
@@ -491,8 +491,8 @@ Section Freeze.
   Qed.
   Hint Rewrite @eval_conditional_add using (omega || assumption)
     : push_basesystem_eval.
-    
-    
+
+
   (*
     The input to [freeze] should be less than 2*m (this can probably
     be accomplished by a single carry_reduce step, for most moduli).
@@ -552,7 +552,7 @@ Section Freeze.
       by (pose proof (Z.div_small (y - (s-c)) s); omega).
       f_equal. ring. }
   Qed.
-  
+
   Lemma eval_freeze {n} c mask m p
         (n_nonzero:n<>0%nat)
         (Hc : 0 < B.Associational.eval c < weight n)
@@ -589,7 +589,7 @@ Section Freeze.
   Qed.
 End Freeze.
 
-  
+
 (*
 (* Just some pretty-printing *)
 Local Notation "fst~ a" := (let (x,_) := a in x) (at level 40, only printing).
diff --git a/src/Curves/Edwards/Pre.v b/src/Curves/Edwards/Pre.v
index 244acc9b5..9f5d5cfab 100644
--- a/src/Curves/Edwards/Pre.v
+++ b/src/Curves/Edwards/Pre.v
@@ -43,4 +43,4 @@ Section Edwards.
     Lemma onCurve_add : onCurve ((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)).
     Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed.
   End Addition.
-End Edwards.
\ No newline at end of file
+End Edwards.
diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v
index 70e8a3f6f..bfd7dce60 100644
--- a/src/Curves/Montgomery/Affine.v
+++ b/src/Curves/Montgomery/Affine.v
@@ -62,4 +62,4 @@ Module M.
       Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
     End MontgomeryWeierstrass.
   End MontgomeryCurve.
-End M.
\ No newline at end of file
+End M.
diff --git a/src/Curves/Montgomery/AffineInstances.v b/src/Curves/Montgomery/AffineInstances.v
index ef5ccd578..049a7695b 100644
--- a/src/Curves/Montgomery/AffineInstances.v
+++ b/src/Curves/Montgomery/AffineInstances.v
@@ -19,7 +19,7 @@ Module M.
     Local Notation "0" := Fzero.
     Local Notation "1" := Fone.
     Local Notation "4" := (1+1+1+1).
-      
+
     Global Instance MontgomeryWeierstrassIsomorphism
            {a b: F}
            (b_nonzero : b <> 0)
@@ -40,7 +40,7 @@ Module M.
         (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero))
         M.zero
         (M.opp(b_nonzero:=b_nonzero))
-        
+
         (M.of_Weierstrass(Haw:=reflexivity _)(Hbw:=reflexivity _)(b_nonzero:=b_nonzero))
         (M.to_Weierstrass(Haw:=reflexivity _)(Hbw:=reflexivity _)(b_nonzero:=b_nonzero)).
     Proof.
diff --git a/src/Curves/Montgomery/AffineProofs.v b/src/Curves/Montgomery/AffineProofs.v
index 4601c3b66..588605c35 100644
--- a/src/Curves/Montgomery/AffineProofs.v
+++ b/src/Curves/Montgomery/AffineProofs.v
@@ -13,7 +13,7 @@ Module M.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}.
-      
+
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
@@ -74,7 +74,7 @@ Module M.
         (M.add(char_ge_3:=_3)(b_nonzero:=_4))
         M.zero
         (M.opp(b_nonzero:=_7))
-        
+
         (M.of_Weierstrass(Haw:=Haw)(Hbw:=Hbw)(b_nonzero:=_5))
         (M.to_Weierstrass(Haw:=Haw)(Hbw:=Hbw)(b_nonzero:=_6)).
     Proof.
diff --git a/src/Curves/Weierstrass/Affine.v b/src/Curves/Weierstrass/Affine.v
index 3a48bf998..cdcb1bec7 100644
--- a/src/Curves/Weierstrass/Affine.v
+++ b/src/Curves/Weierstrass/Affine.v
@@ -17,4 +17,4 @@ Module W.
       cbv [W.coordinates]; break_match; trivial; fsatz.
     Qed.
   End W.
-End W.
\ No newline at end of file
+End W.
diff --git a/src/Curves/Weierstrass/AffineProofs.v b/src/Curves/Weierstrass/AffineProofs.v
index 3401d7b31..2faac22eb 100644
--- a/src/Curves/Weierstrass/AffineProofs.v
+++ b/src/Curves/Weierstrass/AffineProofs.v
@@ -35,7 +35,7 @@ Module W.
            {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive} (* FIXME: shouldn't need we need 4, not 12? *)
            {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)}
       : commutative_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp).
-    Proof using Type. 
+    Proof using Type.
       Time
         cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig];
           repeat match goal with
diff --git a/src/LegacyArithmetic/BaseSystem.v b/src/LegacyArithmetic/BaseSystem.v
index a54bc483f..3f426e98b 100644
--- a/src/LegacyArithmetic/BaseSystem.v
+++ b/src/LegacyArithmetic/BaseSystem.v
@@ -36,4 +36,4 @@ Section BaseSystem.
   Definition decode' bs u  := fold_right accumulate 0 (combine u bs).
   Definition decode := decode' base.
   Definition mul_each u := map (Z.mul u).
-End BaseSystem.
\ No newline at end of file
+End BaseSystem.
diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v
index 9a06109d1..b87df814d 100644
--- a/src/LegacyArithmetic/BaseSystemProofs.v
+++ b/src/LegacyArithmetic/BaseSystemProofs.v
@@ -130,4 +130,4 @@ Section BaseSystemProofs.
             rewrite plus_0_r in *;
             congruence); simpl in HH; congruence. }
   Qed.
-End BaseSystemProofs.
\ No newline at end of file
+End BaseSystemProofs.
diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v
index 681f0b0a9..35540f39a 100644
--- a/src/LegacyArithmetic/Pow2BaseProofs.v
+++ b/src/LegacyArithmetic/Pow2BaseProofs.v
@@ -552,4 +552,4 @@ Section UniformBase.
     rewrite decode_shift_app by auto using uniform_limb_widths_nonneg.
     reflexivity.
   Qed.
-End UniformBase.
\ No newline at end of file
+End UniformBase.
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 83e5645d5..9cde8d004 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -52,4 +52,4 @@ End E.
 Delimit Scope E_scope with E.
 Infix "=" := E.eq : E_scope.
 Infix "+" := E.add : E_scope.
-Infix "*" := E.mul : E_scope.
\ No newline at end of file
+Infix "*" := E.mul : E_scope.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index b8526bb0e..56d5c1bf0 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -54,11 +54,11 @@ Section Ed25519.
 
   Local Instance char_gt_e : (* TODO: prove this in PrimeFieldTheorems *)
     @Ring.char_ge (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0)
-                  (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q) 
+                  (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q)
                   (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.two).
   Proof. intros p ?.
          edestruct (fun p:p = (BinNat.N.succ_pos BinNat.N.zero) \/ p = (BinNat.N.succ_pos BinNat.N.one) => p); subst.
-         { admit. (* 
+         { admit. (*
            p : BinNums.positive
            H : BinPos.Pos.le p (BinNat.N.succ_pos BinNat.N.one)
            ============================
@@ -89,7 +89,7 @@ Section Ed25519.
           (l:=l) (b:=b) (n:=n) (c:=c)
           (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512).
   Proof using Type.
-    split; 
+    split;
       match goal with
       | |- ?P => match goal with [H:P|-_] => exact H end (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *)
       | _ => exact _
diff --git a/src/Spec/Test/X25519.v b/src/Spec/Test/X25519.v
index 15ca468c1..a4fed8dd4 100644
--- a/src/Spec/Test/X25519.v
+++ b/src/Spec/Test/X25519.v
@@ -19,4 +19,4 @@ Proof. vm_decide_no_check. Qed.
 Example testvector_two : F.to_Z (monty
    35156891815674817266734212754503633747128614016119564763269015315466259359304%N
    (F.of_Z _ 8883857351183929894090759386610649319417338800022198945255395922347792736741%Z)) = 39566196721700740701373067725336211924689549479508623342842086701180565506965%Z.
-Proof. vm_decide_no_check. Qed.
\ No newline at end of file
+Proof. vm_decide_no_check. Qed.
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index fc7c64198..9a3a9185d 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -41,7 +41,7 @@ Module W.
     Program Definition zero : point := ∞.
 
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
-    Local Notation "2" := (1+1). Local Notation "3" := (1+2). 
+    Local Notation "2" := (1+1). Local Notation "3" := (1+2).
 
     Program Definition add (P1 P2:point) : point :=
       match coordinates P1, coordinates P2 return F*F+∞ with
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v
index 438f8305e..d9e801a0c 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -254,7 +254,7 @@ Section Ops51.
 
   Hint Opaque freeze : uncps.
   Hint Rewrite freeze_id : uncps.
-  
+
   Definition freeze_sig :
     {freeze : (Z^sz -> Z^sz)%type |
      forall a : Z^sz,
@@ -281,7 +281,7 @@ Section Ops51.
    cbv - [runtime_opp runtime_add runtime_mul runtime_shr runtime_and Let_In Z.add_get_carry Z.zselect].
    reflexivity.
   Defined.
-  
+
   Definition ring_51 :=
     (Ring.ring_by_isomorphism
          (F := F m)
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v
index c09edc891..41b21feb7 100644
--- a/src/Util/CPSUtil.v
+++ b/src/Util/CPSUtil.v
@@ -288,4 +288,4 @@ Module Tuple.
 End Tuple.
 Hint Rewrite @Tuple.map_cps_correct : uncps.
 Hint Rewrite @Tuple.mapi_with_cps_correct @Tuple.mapi_with'_cps_correct
-     using (intros; autorewrite with uncps; auto): uncps.
\ No newline at end of file
+     using (intros; autorewrite with uncps; auto): uncps.
diff --git a/src/Util/Factorize.v b/src/Util/Factorize.v
index 8ccb7d119..12893cd75 100644
--- a/src/Util/Factorize.v
+++ b/src/Util/Factorize.v
@@ -70,4 +70,4 @@ Lemma product_factorize_or_fail (n:N) (factors:list N)
       (H:Logic.eq (factorize_or_fail n) (Some factors))
   : Logic.eq (List.fold_right N.mul 1%N factors) n.
 Proof.  cbv [factorize_or_fail] in H; destruct ((fold_right N.mul 1 (factorize n) =? n)%N) eqn:?;
-          try apply N.eqb_eq; congruence. Qed.
\ No newline at end of file
+          try apply N.eqb_eq; congruence. Qed.
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index 1faa1da95..d76be63aa 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -117,7 +117,7 @@ Module N.
       replace (Z.of_nat 2) with 2%Z by reflexivity.
       omega.
     Qed.
- 
+
     Let ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x).
     Lemma combine_ZNWord : forall sz1 sz2 z1 z2,
         (0 <= Z.of_nat sz1)%Z ->
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 2ccb0455f..74fe96d6b 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -304,4 +304,4 @@ Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z.
 Proof.
   rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1.
   apply Z_div_mod_eq; reflexivity.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/Util/Relations.v b/src/Util/Relations.v
index 7dc654ec3..d6b63b38f 100644
--- a/src/Util/Relations.v
+++ b/src/Util/Relations.v
@@ -56,4 +56,4 @@ Global Instance Symmetric_not {T:Type} (R:T->T->Prop)
        {SymmetricR:Symmetric R} : Symmetric (fun a b => not (R a b)).
 Proof. cbv [Symmetric] in *; repeat intro; eauto. Qed.
 
-Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed.
\ No newline at end of file
+Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed.
diff --git a/src/Util/ZUtil/Zselect.v b/src/Util/ZUtil/Zselect.v
index 0166ce6f4..fa9235a0b 100644
--- a/src/Util/ZUtil/Zselect.v
+++ b/src/Util/ZUtil/Zselect.v
@@ -13,4 +13,4 @@ Module Z.
       try reflexivity; try discriminate.
     rewrite <-Z.eqb_neq in *; congruence.
   Qed.
-End Z.
\ No newline at end of file
+End Z.