diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-10 15:17:20 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:15:49 +0200 |
| commit | a79481b86881be12900b9b16b2f384eb3c402215 (patch) | |
| tree | 4b4a65fc0d1ae5aedb32c8e386164468d1ab2f48 /test-suite/success | |
| parent | 0fe4d837191de481184cc995558ca3774253be0c (diff) | |
romega: discard constructor D_mono (shorter trace + fix a bug)
For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
Diffstat (limited to 'test-suite/success')
| -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. |