diff options
| author | herbelin | 2002-01-21 09:32:08 +0000 |
|---|---|---|
| committer | herbelin | 2002-01-21 09:32:08 +0000 |
| commit | 6f0399df592d58987a65e9e8fce857d80a2c4c22 (patch) | |
| tree | 876d76167251bba132d3f5ba2f61628503ce6020 | |
| parent | 29dbd271e1619b05dbd7677b379332817dbc167d (diff) | |
Ajout test de Pierre Crégut
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2420 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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. |