diff options
| -rw-r--r-- | test-suite/success/Omega.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v new file mode 100644 index 000000000..b8b6f0434 --- /dev/null +++ b/test-suite/success/Omega.v @@ -0,0 +1,11 @@ +(* Submitted by Xavier Urbain 18 Jan 2002 *) + +Require Omega. +Lemma lem : (x,y:Z) + `-5 < x < 5` -> + `-5 < y` -> + `-5 < x+y+5`. +Proof. +Intros x y. +Omega. +Qed. |