1 files changed, 8 insertions, 8 deletions
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.