From 2be53251b7997eda2557a8bb938590f4c8ba24b8 Mon Sep 17 00:00:00 2001
From: mayero
Date: Fri, 20 Apr 2001 19:53:19 +0000
Subject: test Fourier, DiscrR

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1659 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/DiscrR.v  | 41 +++++++++++++++++++++++++++++++++++++++++
 test-suite/success/Fourier.v | 16 ++++++++++++++++
 2 files changed, 57 insertions(+)
 create mode 100644 test-suite/success/DiscrR.v
 create mode 100644 test-suite/success/Fourier.v

diff --git a/test-suite/success/DiscrR.v b/test-suite/success/DiscrR.v
new file mode 100644
index 0000000000..5d12098f22
--- /dev/null
+++ b/test-suite/success/DiscrR.v
@@ -0,0 +1,41 @@
+Require Reals.
+Require DiscrR.
+
+Lemma ex0: ``1<>0``.
+Proof.
+  DiscrR.
+Save.
+
+Lemma ex1: ``0<>2``.
+Proof.
+  DiscrR.
+Save.
+Lemma ex2: ``4<>3``.
+Proof.
+  DiscrR.
+Save.
+
+Lemma ex3: ``3<>5``.
+Proof.
+  DiscrR.
+Save.
+
+Lemma ex4: ``-1<>0``.
+Proof.
+  DiscrR.
+Save.
+
+Lemma ex5: ``-2<>-3``.
+Proof.
+  DiscrR.
+Save.
+
+Lemma ex6: ``8<>-3``.
+Proof.
+  DiscrR.
+Save.
+
+Lemma ex7: ``-8<>3``.
+Proof.
+  DiscrR.
+Save.
diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v
new file mode 100644
index 0000000000..e522cb74f0
--- /dev/null
+++ b/test-suite/success/Fourier.v
@@ -0,0 +1,16 @@
+Require SplitAbsolu.
+Require Fourier.
+ 
+Lemma l1:
+ (x, y, z : R)
+  ``(Rabsolu x-z) <= (Rabsolu x-y)+(Rabsolu y-z)``.
+Intros; SplitAbsolu; Fourier.
+Qed.
+ 
+Lemma l2:
+ (x, y : R)
+ ``x < (Rabsolu y)`` ->
+ ``y < 1`` -> ``x >= 0`` -> ``-y <= 1`` ->  ``(Rabsolu x) <= 1``.
+Intros.
+SplitAbsolu; Fourier.
+Qed.
-- 
cgit v1.2.3