diff options
| author | Vincent Laporte | 2019-10-10 13:37:12 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-22 06:39:10 +0000 |
| commit | a357060331b8806fc2a493e2abc426109f9522a6 (patch) | |
| tree | 48970154f18f936c0f023900cb7eb1e972a1ad45 | |
| parent | 956889d99f58cc63544fca70d81c3242860c7222 (diff) | |
OrderedTypeEx: do not use “omega”
| -rw-r--r-- | theories/Structures/OrderedTypeEx.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index a8e6993a63..cc216b21f8 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -12,7 +12,6 @@ Require Import OrderedType. Require Import ZArith. Require Import PeanoNat. Require Import Ascii String. -Require Import Omega. Require Import NArith Ndec. Require Import Compare_dec. @@ -55,7 +54,7 @@ Module Nat_as_OT <: UsualOrderedType. Proof. unfold lt; intros; apply lt_trans with y; auto. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. - Proof. unfold lt, eq; intros; omega. Qed. + Proof. unfold lt, eq; intros ? ? LT ->; revert LT; apply Nat.lt_irrefl. Qed. Definition compare x y : Compare lt eq x y. Proof. @@ -85,10 +84,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. intros; omega. Qed. + Proof. exact Z.lt_trans. Qed. Lemma lt_not_eq : forall x y, x<y -> ~ x=y. - Proof. intros; omega. Qed. + Proof. intros x y LT ->; revert LT; apply Z.lt_irrefl. Qed. Definition compare x y : Compare lt eq x y. Proof. |