Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/success/LraTest.v b/test-suite/success/LraTest.v
new file mode 100644
index 00000000..bf3a87da
--- /dev/null
+++ b/test-suite/success/LraTest.v
@@ -0,0 +1,14 @@
+Require Import Reals.
+Require Import Lra.
+
+Open Scope R_scope.
+
+Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
+intros; split_Rabs; lra.
+Qed.
+
+Lemma l2 :
+ forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
+intros.
+split_Rabs; lra.
+Qed.