diff options
| author | Maxime Dénès | 2017-05-26 19:20:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-26 19:20:47 +0200 |
| commit | 4445158c58756a315dbbbf5773fc691dd61b61f1 (patch) | |
| tree | 8104ccc88b757002a2437b42cad489901588a75f /test-suite | |
| parent | 06aa7498415ca98a795219a2b1460e812b6bafc6 (diff) | |
| parent | 9bf766d4f66727a638ed2662099d090b5a72200a (diff) | |
Merge PR#666: romega revisited : no more normalization trace, cleaned-up resolution trace
Diffstat (limited to 'test-suite')
| -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 1348bb6238..42730f2e16 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. |