1 files changed, 44 insertions, 44 deletions

diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 1fcf6f61e..5c3a929af 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -151,7 +151,7 @@ Qed.
 (*******************************)
 
 (*********)
-Lemma Rcase_abs : forall r, {r < 0} + {r >= 0}. 
+Lemma Rcase_abs : forall r, {r < 0} + {r >= 0}.
 Proof.
   intro; generalize (Rle_dec 0 r); intro X; elim X; intro; clear X.
   right; apply (Rle_ge 0 r a).
@@ -248,7 +248,7 @@ Proof.
   elimtype False; clear H0; elim H; clear H; generalize H1; unfold Rabs in |- *;
     case (Rcase_abs x); intros; auto.
   clear r H1; generalize (Rplus_eq_compat_l x 0 (- x) H0);
-    rewrite (let (H1, H2) := Rplus_ne x in H1); rewrite (Rplus_opp_r x); 
+    rewrite (let (H1, H2) := Rplus_ne x in H1); rewrite (Rplus_opp_r x);
       trivial.
 Qed.
 
@@ -258,13 +258,13 @@ Proof.
   intros; unfold Rabs in |- *; case (Rcase_abs (x - y));
     case (Rcase_abs (y - x)); intros.
   generalize (Rminus_lt y x r); generalize (Rminus_lt x y r0); intros;
-    generalize (Rlt_asym x y H); intro; elimtype False; 
+    generalize (Rlt_asym x y H); intro; elimtype False;
       auto.
   rewrite (Ropp_minus_distr x y); trivial.
   rewrite (Ropp_minus_distr y x); trivial.
   unfold Rge in r, r0; elim r; elim r0; intros; clear r r0.
   generalize (Ropp_lt_gt_0_contravar (x - y) H); rewrite (Ropp_minus_distr x y);
-    intro; unfold Rgt in H0; generalize (Rlt_asym 0 (y - x) H0); 
+    intro; unfold Rgt in H0; generalize (Rlt_asym 0 (y - x) H0);
       intro; elimtype False; auto.
   rewrite (Rminus_diag_uniq x y H); trivial.
   rewrite (Rminus_diag_uniq y x H0); trivial.
@@ -277,15 +277,15 @@ Proof.
   intros; unfold Rabs in |- *; case (Rcase_abs (x * y)); case (Rcase_abs x);
     case (Rcase_abs y); intros; auto.
   generalize (Rmult_lt_gt_compat_neg_l y x 0 r r0); intro;
-    rewrite (Rmult_0_r y) in H; generalize (Rlt_asym (x * y) 0 r1); 
-      intro; unfold Rgt in H; elimtype False; rewrite (Rmult_comm y x) in H; 
+    rewrite (Rmult_0_r y) in H; generalize (Rlt_asym (x * y) 0 r1);
+      intro; unfold Rgt in H; elimtype False; rewrite (Rmult_comm y x) in H;
         auto.
-  rewrite (Ropp_mult_distr_l_reverse x y); trivial. 
+  rewrite (Ropp_mult_distr_l_reverse x y); trivial.
   rewrite (Rmult_comm x (- y)); rewrite (Ropp_mult_distr_l_reverse y x);
     rewrite (Rmult_comm x y); trivial.
   unfold Rge in r, r0; elim r; elim r0; clear r r0; intros; unfold Rgt in H, H0.
   generalize (Rmult_lt_compat_l x 0 y H H0); intro; rewrite (Rmult_0_r x) in H1;
-    generalize (Rlt_asym (x * y) 0 r1); intro; elimtype False; 
+    generalize (Rlt_asym (x * y) 0 r1); intro; elimtype False;
       auto.
   rewrite H in r1; rewrite (Rmult_0_l y) in r1; generalize (Rlt_irrefl 0);
     intro; elimtype False; auto.
@@ -297,27 +297,27 @@ Proof.
   unfold Rge in r, r1; elim r; elim r1; clear r r1; intros; unfold Rgt in H0, H.
   generalize (Rmult_lt_compat_l y x 0 H0 r0); intro;
     rewrite (Rmult_0_r y) in H1; rewrite (Rmult_comm y x) in H1;
-      generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False; 
+      generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False;
         auto.
   generalize (Rlt_dichotomy_converse x 0 (or_introl (x > 0) r0));
-    generalize (Rlt_dichotomy_converse y 0 (or_intror (y < 0) H0)); 
-      intros; generalize (Rmult_integral x y H); intro; 
-        elim H3; intro; elimtype False; auto.  
+    generalize (Rlt_dichotomy_converse y 0 (or_intror (y < 0) H0));
+      intros; generalize (Rmult_integral x y H); intro;
+        elim H3; intro; elimtype False; auto.
   rewrite H0 in H; rewrite (Rmult_0_r x) in H; unfold Rgt in H;
-    generalize (Rlt_irrefl 0); intro; elimtype False; 
+    generalize (Rlt_irrefl 0); intro; elimtype False;
       auto.
   rewrite H0; rewrite (Rmult_0_r x); rewrite (Rmult_0_r (- x)); trivial.
   unfold Rge in r0, r1; elim r0; elim r1; clear r0 r1; intros;
     unfold Rgt in H0, H.
   generalize (Rmult_lt_compat_l x y 0 H0 r); intro; rewrite (Rmult_0_r x) in H1;
-    generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False; 
+    generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False;
       auto.
   generalize (Rlt_dichotomy_converse y 0 (or_introl (y > 0) r));
-    generalize (Rlt_dichotomy_converse 0 x (or_introl (0 > x) H0)); 
-      intros; generalize (Rmult_integral x y H); intro; 
-        elim H3; intro; elimtype False; auto.  
+    generalize (Rlt_dichotomy_converse 0 x (or_introl (0 > x) H0));
+      intros; generalize (Rmult_integral x y H); intro;
+        elim H3; intro; elimtype False; auto.
   rewrite H0 in H; rewrite (Rmult_0_l y) in H; unfold Rgt in H;
-    generalize (Rlt_irrefl 0); intro; elimtype False; 
+    generalize (Rlt_irrefl 0); intro; elimtype False;
       auto.
   rewrite H0; rewrite (Rmult_0_l y); rewrite (Rmult_0_l (- y)); trivial.
 Qed.
@@ -337,7 +337,7 @@ Proof.
   unfold Rgt in H0; generalize (Rlt_asym 0 (/ r) (Rinv_0_lt_compat r H0));
     intro; elimtype False; auto.
   elimtype False; auto.
-Qed. 
+Qed.
 
 Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x.
 Proof.
@@ -353,7 +353,7 @@ Proof.
   generalize (Ropp_le_ge_contravar 0 (-1) H1).
   rewrite Ropp_involutive; rewrite Ropp_0.
   intro; generalize (Rgt_not_le 1 0 Rlt_0_1); intro; generalize (Rge_le 0 1 H2);
-    intro; elimtype False; auto.  
+    intro; elimtype False; auto.
   ring.
 Qed.
 
@@ -368,7 +368,7 @@ Proof.
   rewrite (Ropp_plus_distr a b); apply (Rplus_le_compat_l (- a) (- b) b);
     unfold Rle in |- *; unfold Rge in r; elim r; intro.
   left; unfold Rgt in H; generalize (Rplus_lt_compat_l (- b) 0 b H); intro;
-    elim (Rplus_ne (- b)); intros v w; rewrite v in H0; 
+    elim (Rplus_ne (- b)); intros v w; rewrite v in H0;
       clear v w; rewrite (Rplus_opp_l b) in H0; apply (Rlt_trans (- b) 0 b H0 H).
   right; rewrite H; apply Ropp_0.
 (**)
@@ -376,13 +376,13 @@ Proof.
     rewrite (Rplus_comm a (- b)); apply (Rplus_le_compat_l (- b) (- a) a);
       unfold Rle in |- *; unfold Rge in r0; elim r0; intro.
   left; unfold Rgt in H; generalize (Rplus_lt_compat_l (- a) 0 a H); intro;
-    elim (Rplus_ne (- a)); intros v w; rewrite v in H0; 
+    elim (Rplus_ne (- a)); intros v w; rewrite v in H0;
       clear v w; rewrite (Rplus_opp_l a) in H0; apply (Rlt_trans (- a) 0 a H0 H).
   right; rewrite H; apply Ropp_0.
 (**)
   elimtype False; generalize (Rplus_ge_compat_l a b 0 r); intro;
     elim (Rplus_ne a); intros v w; rewrite v in H; clear v w;
-      generalize (Rge_trans (a + b) a 0 H r0); intro; clear H; 
+      generalize (Rge_trans (a + b) a 0 H r0); intro; clear H;
         unfold Rge in H0; elim H0; intro; clear H0.
   unfold Rgt in H; generalize (Rlt_asym (a + b) 0 r1); intro; auto.
   absurd (a + b = 0); auto.
@@ -390,7 +390,7 @@ Proof.
 (**)
   elimtype False; generalize (Rplus_lt_compat_l a b 0 r); intro;
     elim (Rplus_ne a); intros v w; rewrite v in H; clear v w;
-      generalize (Rlt_trans (a + b) a 0 H r0); intro; clear H; 
+      generalize (Rlt_trans (a + b) a 0 H r0); intro; clear H;
         unfold Rge in r1; elim r1; clear r1; intro.
   unfold Rgt in H; generalize (Rlt_trans (a + b) 0 (a + b) H0 H); intro;
     apply (Rlt_irrefl (a + b)); assumption.
@@ -399,16 +399,16 @@ Proof.
   rewrite (Rplus_comm a b); rewrite (Rplus_comm (- a) b);
     apply (Rplus_le_compat_l b a (- a)); apply (Rminus_le a (- a));
       unfold Rminus in |- *; rewrite (Ropp_involutive a);
-        generalize (Rplus_lt_compat_l a a 0 r0); clear r r1; 
-          intro; elim (Rplus_ne a); intros v w; rewrite v in H; 
-            clear v w; generalize (Rlt_trans (a + a) a 0 H r0); 
+        generalize (Rplus_lt_compat_l a a 0 r0); clear r r1;
+          intro; elim (Rplus_ne a); intros v w; rewrite v in H;
+            clear v w; generalize (Rlt_trans (a + a) a 0 H r0);
               intro; apply (Rlt_le (a + a) 0 H0).
 (**)
   apply (Rplus_le_compat_l a b (- b)); apply (Rminus_le b (- b));
     unfold Rminus in |- *; rewrite (Ropp_involutive b);
-      generalize (Rplus_lt_compat_l b b 0 r); clear r0 r1; 
-        intro; elim (Rplus_ne b); intros v w; rewrite v in H; 
-          clear v w; generalize (Rlt_trans (b + b) b 0 H r); 
+      generalize (Rplus_lt_compat_l b b 0 r); clear r0 r1;
+        intro; elim (Rplus_ne b); intros v w; rewrite v in H;
+          clear v w; generalize (Rlt_trans (b + b) b 0 H r);
             intro; apply (Rlt_le (b + b) 0 H0).
 (**)
   unfold Rle in |- *; right; reflexivity.
@@ -430,25 +430,25 @@ Proof.
 Qed.
 
 (* ||a|-|b||<=|a-b| *)
-Lemma Rabs_triang_inv2 : forall a b:R, Rabs (Rabs a - Rabs b) <= Rabs (a - b). 
+Lemma Rabs_triang_inv2 : forall a b:R, Rabs (Rabs a - Rabs b) <= Rabs (a - b).
 Proof.
   cut
-    (forall a b:R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)). 
+    (forall a b:R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)).
   intros; destruct (Rtotal_order (Rabs a) (Rabs b)) as [Hlt| [Heq| Hgt]].
   rewrite <- (Rabs_Ropp (Rabs a - Rabs b)); rewrite <- (Rabs_Ropp (a - b));
-    do 2 rewrite Ropp_minus_distr. 
-  apply H; left; assumption. 
+    do 2 rewrite Ropp_minus_distr.
+  apply H; left; assumption.
   rewrite Heq; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
-    apply Rabs_pos. 
-  apply H; left; assumption. 
-  intros; replace (Rabs (Rabs a - Rabs b)) with (Rabs a - Rabs b). 
-  apply Rabs_triang_inv. 
+    apply Rabs_pos.
+  apply H; left; assumption.
+  intros; replace (Rabs (Rabs a - Rabs b)) with (Rabs a - Rabs b).
+  apply Rabs_triang_inv.
   rewrite (Rabs_right (Rabs a - Rabs b));
     [ reflexivity
       | apply Rle_ge; apply Rplus_le_reg_l with (Rabs b); rewrite Rplus_0_r;
-        replace (Rabs b + (Rabs a - Rabs b)) with (Rabs a); 
-        [ assumption | ring ] ]. 
-Qed. 
+        replace (Rabs b + (Rabs a - Rabs b)) with (Rabs a);
+        [ assumption | ring ] ].
+Qed.
 
 (*********)
 Lemma Rabs_def1 : forall x a:R, x < a -> - a < x -> Rabs x < a.
@@ -464,13 +464,13 @@ Lemma Rabs_def2 : forall x a:R, Rabs x < a -> x < a /\ - a < x.
 Proof.
   unfold Rabs in |- *; intro x; case (Rcase_abs x); intros.
   generalize (Ropp_gt_lt_0_contravar x r); unfold Rgt in |- *; intro;
-    generalize (Rlt_trans 0 (- x) a H0 H); intro; split. 
+    generalize (Rlt_trans 0 (- x) a H0 H); intro; split.
   apply (Rlt_trans x 0 a r H1).
   generalize (Ropp_lt_gt_contravar (- x) a H); rewrite (Ropp_involutive x);
     unfold Rgt in |- *; trivial.
   fold (a > x) in H; generalize (Rgt_ge_trans a x 0 H r); intro;
     generalize (Ropp_lt_gt_0_contravar a H0); intro; fold (0 > - a) in |- *;
-      generalize (Rge_gt_trans x 0 (- a) r H1); unfold Rgt in |- *; 
+      generalize (Rge_gt_trans x 0 (- a) r H1); unfold Rgt in |- *;
         intro; split; assumption.
 Qed.
 
@@ -508,7 +508,7 @@ Proof.
   intros p0; rewrite Rabs_Ropp.
   apply Rabs_right; auto with real zarith.
 Qed.
- 
+
 Lemma abs_IZR : forall z, IZR (Zabs z) = Rabs (IZR z).
 Proof.
   intros.