Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 18 insertions, 2 deletions

diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
index 1348bb62..3ddf6a40 100644
--- a/test-suite/success/ROmega0.v
+++ b/test-suite/success/ROmega0.v
@@ -132,21 +132,37 @@ intros.
 romega.
 Qed.
 
-(* Magaud #240 *)
+(* Magaud BZ#240 *)
 
 Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+Proof.
 intros.
 romega.
 Qed.
 
 Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+Proof.
 intros x y.
 romega.
 Qed.
 
-(* Besson #1298 *)
+(* Besson BZ#1298 *)
 
 Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False.
+Proof.
 intros.
 romega.
 Qed.
+
+(* Letouzey, May 2017 *)
+
+Lemma test_romega10 : forall x a a' b b',
+ a' <= b ->
+ a <= b' ->
+ b < b' ->
+ a < a' ->
+ a <= x < b' <-> a <= x < b \/ a' <= x < b'.
+Proof.
+ intros.
+ romega.
+Qed.