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 000000000..bf3a87da2
--- /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.