diff options
| -rw-r--r-- | test-suite/success/Omega.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index b5dfea1e97..2b5dd9a1a7 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -17,3 +17,11 @@ Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`. Intro. Omega. Qed. + +(* Proposed by Jean-Christophe Filliātre *) + +Lemma lem3 : (x,y:Z) `x = y` -> `x+x = y+y`. +Proof. +Intros. +Omega. +Qed. |