Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 8 insertions, 12 deletions

diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v
index f1f7ae08..2d184fef 100644
--- a/test-suite/success/Fourier.v
+++ b/test-suite/success/Fourier.v
@@ -1,16 +1,12 @@
-Require Rfunctions.
-Require Fourier.
+Require Import Rfunctions.
+Require Import Fourier.
  
-Lemma l1:
- (x, y, z : R)
-  ``(Rabsolu x-z) <= (Rabsolu x-y)+(Rabsolu y-z)``.
-Intros; SplitAbsolu; Fourier.
+Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
+intros; split_Rabs; fourier.
 Qed.
  
-Lemma l2:
- (x, y : R)
- ``x < (Rabsolu y)`` ->
- ``y < 1`` -> ``x >= 0`` -> ``-y <= 1`` ->  ``(Rabsolu x) <= 1``.
-Intros.
-SplitAbsolu; Fourier.
+Lemma l2 :
+ forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
+intros.
+split_Rabs; fourier.
 Qed.