1 files changed, 19 insertions, 19 deletions

diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index fe8fcc924..56a854d6f 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
@@ -31,7 +31,7 @@ Qed.
 Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m).
 Proof.
   intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x);
-    rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; 
+    rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm;
       trivial with arith.
 Qed.
 
@@ -53,7 +53,7 @@ Qed.
 (** Other specific variants of theorems dedicated for the Omega tactic *)
 
 Lemma new_var : forall x : Z, exists y : Z, x = y.
-intros x; exists x; trivial with arith. 
+intros x; exists x; trivial with arith.
 Qed.
 
 Lemma OMEGA1 : forall x y : Z, x = y -> 0 <= x -> 0 <= y.
@@ -62,7 +62,7 @@ Qed.
 
 Lemma OMEGA2 : forall x y : Z, 0 <= x -> 0 <= y -> 0 <= x + y.
 exact Zplus_le_0_compat.
-Qed. 
+Qed.
 
 Lemma OMEGA3 : forall x y k : Z, k > 0 -> x = y * k -> x = 0 -> y = 0.
 
@@ -82,11 +82,11 @@ unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0);
        [ rewrite H3; unfold Zgt in |- *; simpl in |- *; discriminate
        | apply Zle_gt_trans with x;
           [ pattern x at 1 in |- *; rewrite <- (Zplus_0_l x);
-             apply Zplus_le_compat_r; rewrite Zmult_comm; 
+             apply Zplus_le_compat_r; rewrite Zmult_comm;
              generalize H4; unfold Zgt in |- *; case y;
              [ simpl in |- *; intros H7; discriminate H7
              | intros p H7; rewrite <- (Zmult_0_r (Zpos p));
-                unfold Zle in |- *; rewrite Zcompare_mult_compat; 
+                unfold Zle in |- *; rewrite Zcompare_mult_compat;
                 exact H6
              | simpl in |- *; intros p H7; discriminate H7 ]
           | assumption ] ]
@@ -116,7 +116,7 @@ Lemma OMEGA8 : forall x y : Z, 0 <= x -> 0 <= y -> x = - y -> x = 0.
 intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1);
  [ intros H4; absurd (0 < x);
     [ change (0 >= x) in |- *; apply Zle_ge; apply Zplus_le_reg_l with y;
-       rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r; 
+       rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r;
        assumption
     | assumption ]
  | intros H4; rewrite H4; trivial with arith ].
@@ -143,7 +143,7 @@ Lemma OMEGA11 :
  (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
 
 intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
- repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; 
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
  trivial with arith.
 Qed.
 
@@ -152,7 +152,7 @@ Lemma OMEGA12 :
  l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
 
 intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
- repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; 
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
  rewrite Zplus_permute; trivial with arith.
 Qed.
 
@@ -166,7 +166,7 @@ intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1);
  rewrite Zplus_opp_r; rewrite Zmult_0_r; rewrite Zplus_0_r;
  trivial with arith.
 Qed.
- 
+
 Lemma OMEGA14 :
  forall (v l1 l2 : Z) (x : positive),
  v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2.
@@ -188,14 +188,14 @@ Qed.
 Lemma OMEGA16 : forall v c l k : Z, (v * c + l) * k = v * (c * k) + l * k.
 
 intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
- repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; 
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
  trivial with arith.
 Qed.
 
 Lemma OMEGA17 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
 
 unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1;
- apply Zplus_reg_l with (y * z); rewrite Zplus_comm; 
+ apply Zplus_reg_l with (y * z); rewrite Zplus_comm;
  rewrite H3; rewrite H2; auto with arith.
 Qed.
 
@@ -213,7 +213,7 @@ unfold Zne in |- *; intros x H; elim (Zle_or_lt 0 x);
        rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption
     | intros H2; absurd (x = 0); auto with arith ]
  | intros H1; right; rewrite <- Zopp_eq_mult_neg_1; rewrite Zplus_comm;
-    apply Zle_left; apply Zsucc_le_reg; simpl in |- *; 
+    apply Zle_left; apply Zsucc_le_reg; simpl in |- *;
     apply Zlt_le_succ; auto with arith ].
 Qed.
 
@@ -229,7 +229,7 @@ Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop)
 Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop)
   (H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p).
 
-Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop) 
+Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop)
   (H : P (n + m + p)) := eq_ind_r P H (Zplus_assoc n m p).
 
 Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop)
@@ -257,7 +257,7 @@ Definition fast_OMEGA13 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
 
 Definition fast_OMEGA14 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
   (H : P (l1 + l2)) := eq_ind_r P H (OMEGA14 v l1 l2 x).
-Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop) 
+Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop)
   (H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x).
 
 Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop)
@@ -272,18 +272,18 @@ Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop)
 Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) :=
   eq_ind_r P H (Zopp_involutive x).
 
-Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop) 
+Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop)
   (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y).
 
 Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop)
   (H : P (n * p + m * p)) := eq_ind_r P H (Zmult_plus_distr_l n m p).
-Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop) 
+Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop)
   (H : P (x * - y)) := eq_ind_r P H (Zmult_opp_comm x y).
 
 Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop)
   (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p).
 
-Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop) 
+Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop)
   (H : P (x * 2)) := eq_ind_r P H (Zred_factor1 x).
 
 Definition fast_Zred_factor2 (x y : Z) (P : Z -> Prop)
@@ -295,8 +295,8 @@ Definition fast_Zred_factor3 (x y : Z) (P : Z -> Prop)
 Definition fast_Zred_factor4 (x y z : Z) (P : Z -> Prop)
   (H : P (x * (y + z))) := eq_ind_r P H (Zred_factor4 x y z).
 
-Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop) 
+Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
   (H : P y) := eq_ind_r P H (Zred_factor5 x y).
 
-Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop) 
+Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
   (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).