blob: 2b5dd9a1a707c62dc6496d787fc595ee6645806c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Require Omega.
(* Submitted by Xavier Urbain 18 Jan 2002 *)
Lemma lem1 : (x,y:Z)
`-5 < x < 5` ->
`-5 < y` ->
`-5 < x+y+5`.
Proof.
Intros x y.
Omega.
Qed.
(* Proposed by Pierre Cr�gut *)
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.
|
