From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Sat, 18 Aug 2007 20:34:57 +0000
Subject: Imported Upstream version 8.1.pl1+dfsg

---
 test-suite/success/ROmega2.v | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'test-suite/success/ROmega2.v')

diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
index 9d47c9f6..a3be2898 100644
--- a/test-suite/success/ROmega2.v
+++ b/test-suite/success/ROmega2.v
@@ -4,6 +4,20 @@ Require Import ZArith ROmega.
 
 Open Scope Z_scope.
 
+
+(* First a simplified version used during debug of romega on Test46 *)
+Lemma Test46_simplified : 
+forall v1 v2 v5 : Z,
+0 = v2 + v5 ->
+0 < v5 ->
+0 < v2 ->
+4*v2 <> 5*v1.
+intros.
+romega.
+Qed.
+
+
+(* The complete problem *)
 Lemma Test46 : 
 forall v1 v2 v3 v4 v5 : Z,
 ((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
@@ -23,6 +37,5 @@ forall v1 v2 v3 v4 v5 : Z,
 ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
 -> False.
 intros.
-(*romega.*)
-Admitted.
-
+romega.
+Qed.
-- 
cgit v1.2.3