From 8365199914dd7867effa34d3956e1c92e849b606 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 20 May 2006 21:34:27 +0000 Subject: auto with zarith genere des sous-lemmes silencieusement, et ... <: ... with E:=Z_as_OT n'aime pas ca git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8836 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/OrderedTypeEx.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theories') diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index cee0413b1..012b6bfb3 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -15,6 +15,7 @@ Require Import OrderedType. Require Import ZArith. +Require Import Omega. Require Import NArith Ndec. Require Import Compare_dec. @@ -85,10 +86,10 @@ Module Z_as_OT <: UsualOrderedType. Definition lt (x y:Z) := (x y x ~ x=y. - Proof. auto with zarith. Qed. + Proof. intros; omega. Qed. Definition compare : forall x y, Compare lt eq x y. Proof. @@ -100,7 +101,6 @@ Module Z_as_OT <: UsualOrderedType. End Z_as_OT. - (** [positive] is an ordered type with respect to the usual order on natural numbers. *) Open Scope positive_scope. @@ -118,7 +118,7 @@ Module Positive_as_OT <: UsualOrderedType. Proof. unfold lt; intros x y z. change ((Zpos x < Zpos y)%Z -> (Zpos y < Zpos z)%Z -> (Zpos x < Zpos z)%Z). - auto with zarith. + omega. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. -- cgit v1.2.3