diff options
Diffstat (limited to 'test-suite/success/ROmega0.v')
| -rw-r--r-- | test-suite/success/ROmega0.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 1348bb623..42730f2e1 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -135,11 +135,13 @@ Qed. (* Magaud #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. @@ -147,6 +149,20 @@ Qed. (* Besson #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. |