From d20c3c79eddab8599c91867554117b3cafbc3b1c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Jan 2006 19:53:13 +0000
Subject: Test conflictuel - ajouté pour mémoire

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7849 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Omega.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 6df2f83d18..2d29a8356b 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -85,3 +85,12 @@ Lemma lem9 :
 intros;  omega.
 Qed.
 
+(* Check that the interpretation of mult on nat enforces its positivity *)
+(* Submitted by Hubert Thierry (bug #743) *)
+(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z"
+Require Omega.
+Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))).
+Proof.
+Intros; Omega.
+Qed.
+*)
-- 
cgit v1.2.3