diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-20 21:34:27 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-20 21:34:27 +0000 |
| commit | 8365199914dd7867effa34d3956e1c92e849b606 (patch) | |
| tree | 658c676342ad6a7efc99af0cc88f0efcf784b0a3 /theories | |
| parent | f7656793f06116377eea14b2c8f9b98db608ec5e (diff) | |
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
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/FSets/OrderedTypeEx.v | 8 |
1 files changed, 4 insertions, 4 deletions
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). Lemma lt_trans : forall x y z, x<y -> y<z -> x<z. - Proof. auto with zarith. Qed. + Proof. intros; omega. Qed. Lemma lt_not_eq : forall x y, x<y -> ~ 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. |