diff --git a/examples/lra_examples.v b/examples/lra_examples.v
index 7554ae5..9574e31 100644
--- a/examples/lra_examples.v
+++ b/examples/lra_examples.v
@@ -109,6 +109,11 @@ Proof.
 lra.
 Qed.
 
+Lemma test_rfstr (x : rat) : (x <= 2%:R) || true = true.
+Proof.
+lra.
+Qed.
+
 End Tests.
 
 (* Examples from the test suite of Coq *)