summaryrefslogtreecommitdiff
path: root/test-suite/success/ROmega0.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /test-suite/success/ROmega0.v
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'test-suite/success/ROmega0.v')
-rw-r--r--test-suite/success/ROmega0.v35
1 files changed, 19 insertions, 16 deletions
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
index 0efca1e1..86cf49cb 100644
--- a/test-suite/success/ROmega0.v
+++ b/test-suite/success/ROmega0.v
@@ -8,16 +8,16 @@ Lemma test_romega_0 :
0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
Proof.
intros.
-(*romega.*)
-Admitted.
+romega.
+Qed.
Lemma test_romega_0b :
forall m m',
0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
Proof.
intros m m'.
-(*romega.*)
-Admitted.
+romega.
+Qed.
Lemma test_romega_1 :
forall (z z1 z2 : Z),
@@ -42,8 +42,8 @@ Lemma test_romega_1b :
z >= 0.
Proof.
intros z z1 z2.
-(* romega. *)
-Admitted.
+romega.
+Qed.
Lemma test_romega_2 : forall a b c:Z,
0<=a-b<=1 -> b-c<=2 -> a-c<=3.
@@ -56,8 +56,8 @@ Lemma test_romega_2b : forall a b c:Z,
0<=a-b<=1 -> b-c<=2 -> a-c<=3.
Proof.
intros a b c.
-(*romega.*)
-Admitted.
+romega.
+Qed.
Lemma test_romega_3 : forall a b h hl hr ha hb,
0 <= ha - hl <= 1 ->
@@ -115,22 +115,22 @@ Qed.
Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
Proof.
intros z.
-(*romega. *)
-Admitted.
+romega.
+Qed.
Lemma test_romega_7 : forall z,
0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
Proof.
intros.
-(*romega.*)
-Admitted.
+romega.
+Qed.
Lemma test_romega_7b : forall z,
0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
Proof.
intros.
-(*romega.*)
-Admitted.
+romega.
+Qed.
(* Magaud #240 *)
@@ -144,6 +144,9 @@ intros x y.
romega.
Qed.
+(* Besson #1298 *)
-
-
+Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False.
+intros.
+romega.
+Qed.