diff options
| -rw-r--r-- | test-suite/success/Omega.v | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index b8b6f04345..b5dfea1e97 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -1,7 +1,8 @@ +Require Omega. + (* Submitted by Xavier Urbain 18 Jan 2002 *) -Require Omega. -Lemma lem : (x,y:Z) +Lemma lem1 : (x,y:Z) `-5 < x < 5` -> `-5 < y` -> `-5 < x+y+5`. @@ -9,3 +10,10 @@ Proof. Intros x y. Omega. Qed. + +(* Proposed by Pierre Crégut *) + +Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`. +Intro. +Omega. +Qed. |