test Fourier, DiscrR

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1659 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 57 insertions, 0 deletions

diff --git a/test-suite/success/DiscrR.v b/test-suite/success/DiscrR.v
new file mode 100644
index 000000000..5d12098f2
--- /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 000000000..e522cb74f
--- /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.