diff options
Diffstat (limited to 'test-suite/success/ROmega0.v')
| -rw-r--r-- | test-suite/success/ROmega0.v | 20 |
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. |