Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 41 insertions, 0 deletions

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