ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12714 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 173 insertions, 187 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 9b8485519..e4fcf2eb1 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -149,9 +149,9 @@ Program Instance iff_Transitive : Transitive iff.
 
 (** Leibniz equality. *)
 
-Program Instance eq_Reflexive : Reflexive (@eq A).
-Program Instance eq_Symmetric : Symmetric (@eq A).
-Program Instance eq_Transitive : Transitive (@eq A).
+Instance eq_Reflexive : Reflexive (@eq A) := eq_refl.
+Instance eq_Symmetric : Symmetric (@eq A) := eq_sym.
+Instance eq_Transitive : Transitive (@eq A) := eq_trans.
 
 (** Various combinations of reflexivity, symmetry and transitivity. *)
 
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 835f79585..bc1dadcd9 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -12,17 +12,11 @@
 
 
 Require Import ZAxioms ZProperties.
-Require Import ZArith_base.
+Require Import BinInt Zcompare Zorder ZArith_dec Zbool.
 
 Local Open Scope Z_scope.
 
-(** * Implementation of [ZAxiomsSig] by [BinInt.Z] *)
-
-Module ZBinAxiomsMod <: ZAxiomsExtSig.
-
-(** Bi-directional induction. *)
-
-Theorem bi_induction :
+Theorem Z_bi_induction :
   forall A : Z -> Prop, Proper (eq ==> iff) A ->
     A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
 Proof.
@@ -32,6 +26,34 @@ intros; rewrite <- Zsucc_succ'. now apply -> AS.
 intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply <- AS.
 Qed.
 
+
+(** * Implementation of [ZAxiomsSig] by [BinInt.Z] *)
+
+Module Z
+ <: ZAxiomsExtSig <: UsualOrderedTypeFull <: TotalOrder
+ <: UsualDecidableTypeFull.
+
+Definition t := Z.
+Definition eqb := Zeq_bool.
+Definition zero := 0.
+Definition succ := Zsucc.
+Definition pred := Zpred.
+Definition add := Zplus.
+Definition sub := Zminus.
+Definition mul := Zmult.
+Definition lt := Zlt.
+Definition le := Zle.
+Definition compare := Zcompare.
+Definition min := Zmin.
+Definition max := Zmax.
+Definition opp := Zopp.
+Definition abs := Zabs.
+Definition sgn := Zsgn.
+
+Definition eq_dec := Z_eq_dec.
+
+Definition bi_induction := Z_bi_induction.
+
 (** Basic operations. *)
 
 Definition eq_equiv : Equivalence (@eq Z) := eq_equivalence.
@@ -50,6 +72,10 @@ Definition sub_succ_r := Zminus_succ_r.
 Definition mul_0_l := Zmult_0_l.
 Definition mul_succ_l := Zmult_succ_l.
 
+(** Boolean Equality *)
+
+Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
+
 (** Order *)
 
 Program Instance lt_wd : Proper (eq==>eq==>iff) Zlt.
@@ -58,6 +84,12 @@ Definition lt_eq_cases := Zle_lt_or_eq_iff.
 Definition lt_irrefl := Zlt_irrefl.
 Definition lt_succ_r := Zlt_succ_r.
 
+(** Comparison *)
+
+Definition compare_spec := Zcompare_spec.
+
+(** Minimum and maximum *)
+
 Definition min_l := Zmin_l.
 Definition min_r := Zmin_r.
 Definition max_l := Zmax_l.
@@ -76,35 +108,34 @@ Definition opp_succ := Zopp_succ.
 Definition abs_eq := Zabs_eq.
 Definition abs_neq := Zabs_non_eq.
 
-Lemma sgn_null : forall x, x = 0 -> Zsgn x = 0.
-Proof. intros. apply <- Zsgn_null; auto. Qed.
-Lemma sgn_pos : forall x, 0 < x -> Zsgn x = 1.
-Proof. intros. apply <- Zsgn_pos; auto. Qed.
-Lemma sgn_neg : forall x, x < 0 -> Zsgn x = -1.
-Proof. intros. apply <- Zsgn_neg; auto. Qed.
+Definition sgn_null := Zsgn_0.
+Definition sgn_pos := Zsgn_1.
+Definition sgn_neg := Zsgn_m1.
 
-(** The instantiation of operations.
-    Placing them at the very end avoids having indirections in above lemmas. *)
+(** We define [eq] only here to avoid refering to this [eq] above. *)
 
-Definition t := Z.
 Definition eq := (@eq Z).
-Definition zero := 0.
-Definition succ := Zsucc.
-Definition pred := Zpred.
-Definition add := Zplus.
-Definition sub := Zminus.
-Definition mul := Zmult.
-Definition lt := Zlt.
-Definition le := Zle.
-Definition min := Zmin.
-Definition max := Zmax.
-Definition opp := Zopp.
-Definition abs := Zabs.
-Definition sgn := Zsgn.
 
-End ZBinAxiomsMod.
+(** Now the generic properties. *)
+
+Include ZPropFunct
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+
+End Z.
+
+(** * An [order] tactic for integers *)
+
+Ltac z_order := Z.order.
+
+(** Note that [z_order] is domain-agnostic: it will not prove
+    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
 
-Module Export ZBinPropMod := ZPropFunct ZBinAxiomsMod.
+Section TestOrder.
+ Let test : forall x y, x<=y -> y<=x -> x=y.
+ Proof.
+ z_order.
+ Qed.
+End TestOrder.
 
 (** Z forms a ring *)
 
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 487b1d0cc..3d4430b9e 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -176,8 +176,7 @@ Module Type UsualEq <: Eq := Typ <+ HasUsualEq.
 
 Module Type UsualIsEq (E:UsualEq) <: IsEq E.
  (* No Instance syntax to avoid saturating the Equivalence tables *)
- Lemma eq_equiv : Equivalence E.eq.
- Proof. exact eq_equivalence. Qed.
+ Definition eq_equiv : Equivalence E.eq := eq_equivalence.
 End UsualIsEq.
 
 Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index 56f1d5ded..d7c0deb94 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -14,7 +14,7 @@
 (* $Id$ *)
 
 Require Import Orders NatOrderedType POrderedType NOrderedType
- ZOrderedType RelationPairs EqualitiesFacts.
+ ZBinary RelationPairs EqualitiesFacts.
 
 (** * Examples of Ordered Type structures. *)
 
@@ -24,7 +24,7 @@ Require Import Orders NatOrderedType POrderedType NOrderedType
 Module Nat_as_OT := NatOrderedType.Nat_as_OT.
 Module Positive_as_OT := POrderedType.Positive_as_OT.
 Module N_as_OT := NOrderedType.N_as_OT.
-Module Z_as_OT := ZOrderedType.Z_as_OT.
+Module Z_as_OT := ZBinary.Z.
 
 (** An OrderedType can now directly be seen as a DecidableType *)
 
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index d976b01c6..2807532ca 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1118,6 +1118,21 @@ Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 
 (**********************************************************************)
+(** * Minimum and maximum *)
+
+Unboxed Definition Zmax (n m:Z) :=
+  match n ?= m with
+    | Eq | Gt => n
+    | Lt => m
+  end.
+
+Unboxed Definition Zmin (n m:Z) :=
+  match n ?= m with
+    | Eq | Lt => n
+    | Gt => m
+  end.
+
+(**********************************************************************)
 (** * Absolute value on integers *)
 
 Definition Zabs_nat (x:Z) : nat :=
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 5747afc9a..a263ab379 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -21,3 +21,7 @@ Require Export Zdiv.
 Require Export Zlogarithm.
 
 Export ZArithRing.
+
+(** Final Z module, cumulating ZBinary.Z, Zminmax.Z, and Zdiv.Z *)
+
+Module Z := Zdiv.Z.
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index cd866c375..1ce877b18 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -34,3 +34,5 @@ Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
   Zmult_plus_distr_r: zarith.
 
 Require Export Zhints.
+
+Module Z := Zminmax.Z.
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
index bea0429dd..282333c13 100644
--- a/theories/ZArith/ZOdiv.v
+++ b/theories/ZArith/ZOdiv.v
@@ -9,7 +9,7 @@
 
 Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms.
 Require Export ZOdiv_def.
-Require Zdiv Binary.ZBinary ZDivTrunc.
+Require Zdiv ZBinary ZDivTrunc.
 
 Open Scope Z_scope.
 
@@ -246,7 +246,7 @@ Qed.
 (** We know enough to prove that [ZOdiv] and [ZOmod] are instances of
     one of the abstract Euclidean divisions of Numbers. *)
 
-Module ZODiv <: ZDivTrunc.ZDiv ZBinary.ZBinAxiomsMod.
+Module ZODiv <: ZDivTrunc.ZDiv ZBinary.Z.
  Definition div := ZOdiv.
  Definition modulo := ZOmod.
  Local Obligation Tactic := simpl_relation.
@@ -259,11 +259,11 @@ Module ZODiv <: ZDivTrunc.ZDiv ZBinary.ZBinAxiomsMod.
  Definition mod_opp_r := fun a b (_:b<>0) => ZOmod_opp_r a b.
 End ZODiv.
 
-Module ZODivMod := ZBinary.ZBinAxiomsMod <+ ZODiv.
+Module ZODivMod := ZBinary.Z <+ ZODiv.
 
 (** We hence benefit from generic results about this abstract division. *)
 
-Module Z := ZDivTrunc.ZDivPropFunct ZODivMod ZBinary.ZBinPropMod.
+Module Z := ZDivTrunc.ZDivPropFunct ZODivMod ZBinary.Z.
 
 (** * Unicity results *)
 
diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v
deleted file mode 100644
index 570e2a4d6..000000000
--- a/theories/ZArith/ZOrderedType.v
+++ /dev/null
@@ -1,60 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import BinInt Zcompare Zorder Zbool ZArith_dec
- Equalities Orders OrdersTac.
-
-Local Open Scope Z_scope.
-
-(** * DecidableType structure for binary integers *)
-
-Module Z_as_UBE <: UsualBoolEq.
- Definition t := Z.
- Definition eq := @eq Z.
- Definition eqb := Zeq_bool.
- Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
-End Z_as_UBE.
-
-Module Z_as_DT <: UsualDecidableTypeFull := Make_UDTF Z_as_UBE.
-
-(** Note that the last module fulfills by subtyping many other
-    interfaces, such as [DecidableType] or [EqualityType]. *)
-
-
-(** * OrderedType structure for binary integers *)
-
-Module Z_as_OT <: OrderedTypeFull.
- Include Z_as_DT.
- Definition lt := Zlt.
- Definition le := Zle.
- Definition compare := Zcompare.
-
- Instance lt_strorder : StrictOrder Zlt.
- Proof. split; [ exact Zlt_irrefl | exact Zlt_trans ]. Qed.
-
- Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Zlt.
- Proof. repeat red; intros; subst; auto. Qed.
-
- Definition le_lteq := Zle_lt_or_eq_iff.
- Definition compare_spec := Zcompare_spec.
-
-End Z_as_OT.
-
-(** Note that [Z_as_OT] can also be seen as a [UsualOrderedType]
-   and a [OrderedType] (and also as a [DecidableType]). *)
-
-
-
-(** * An [order] tactic for integers *)
-
-Module ZOrder := OTF_to_OrderTac Z_as_OT.
-Ltac z_order := ZOrder.order.
-
-(** Note that [z_order] is domain-agnostic: it will not prove
-    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
-
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 36eb41104..ba454c327 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -23,21 +23,12 @@ Open Local Scope Z_scope.
 (**********************************************************************)
 (** * Properties of absolute value *)
 
-Lemma Zabs_eq : forall n:Z, 0 <= n -> Zabs n = n.
-Proof.
-  intro x; destruct x; auto with arith.
-  compute in |- *; intros; absurd (Gt = Gt); trivial with arith.
-Qed.
-
-Lemma Zabs_non_eq : forall n:Z, n <= 0 -> Zabs n = - n.
-Proof.
-  intro x; destruct x; auto with arith.
-  compute in |- *; intros; absurd (Gt = Gt); trivial with arith.
-Qed.
+Notation Zabs_eq := Zabs_eq (only parsing). (* 0 <= n -> Zabs n = n *)
+Notation Zabs_non_eq := Zabs_non_eq (only parsing). (* n <= 0 -> Zabs n = -n *)
 
 Theorem Zabs_Zopp : forall n:Z, Zabs (- n) = Zabs n.
 Proof.
-  intros z; case z; simpl in |- *; auto.
+  intros z; case z; simpl; auto.
 Qed.
 
 (** * Proving a property of the absolute value by cases *)
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 3e611d543..7c2148cc4 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -521,3 +521,62 @@ Proof.
     apply Zmult_compare_compat_l; assumption.
 Qed.
 
+(*************************)
+(** * Basic properties of minimum and maximum *)
+
+Lemma Zmax_l : forall x y, y<=x -> Zmax x y = x.
+Proof.
+ unfold Zle, Zmax. intros x y. rewrite <- (Zcompare_antisym x y).
+ destruct (x ?= y); intuition.
+Qed.
+
+Lemma Zmax_r : forall x y, x<=y -> Zmax x y = y.
+Proof.
+ unfold Zle, Zmax. intros x y. generalize (Zcompare_Eq_eq x y).
+ destruct (x ?= y); intuition.
+Qed.
+
+Lemma Zmin_l : forall x y, x<=y -> Zmin x y = x.
+Proof.
+ unfold Zle, Zmin. intros x y. generalize (Zcompare_Eq_eq x y).
+ destruct (x ?= y); intuition.
+Qed.
+
+Lemma Zmin_r : forall x y, y<=x -> Zmin x y = y.
+Proof.
+ unfold Zle, Zmin. intros x y.
+ rewrite <- (Zcompare_antisym x y). generalize (Zcompare_Eq_eq x y).
+ destruct (x ?= y); intuition.
+Qed.
+
+
+(**************************)
+(** * Basic properties of [Zabs] *)
+
+Lemma Zabs_eq : forall n:Z, 0 <= n -> Zabs n = n.
+Proof.
+ destruct n; auto. now destruct 1.
+Qed.
+
+Lemma Zabs_non_eq : forall n:Z, n <= 0 -> Zabs n = - n.
+Proof.
+ destruct n; auto. now destruct 1.
+Qed.
+
+(**************************)
+(** * Basic properties of [Zsign] *)
+
+Lemma Zsgn_0 : forall x, x = 0 -> Zsgn x = 0.
+Proof.
+ intros. now subst.
+Qed.
+
+Lemma Zsgn_1 : forall x, 0 < x -> Zsgn x = 1.
+Proof.
+ destruct x; auto; discriminate.
+Qed.
+
+Lemma Zsgn_m1 : forall x, x < 0 -> Zsgn x = -1.
+Proof.
+ destruct x; auto; discriminate.
+Qed.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index e9e963f97..4477d559e 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -19,7 +19,7 @@
 
 Require Export ZArith_base.
 Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms.
-Require ZDivFloor ZBinary.
+Require ZDivFloor.
 Open Local Scope Z_scope.
 
 (** * Definitions of Euclidian operations *)
@@ -301,9 +301,11 @@ Proof.
 Qed.
 
 (** We know enough to prove that [Zdiv] and [Zmod] are instances of
-    one of the abstract Euclidean divisions of Numbers. *)
+    one of the abstract Euclidean divisions of Numbers.
+    We hence benefit from generic results about this abstract division. *)
+
+Module Z.
 
-Module ZDiv <: ZDivFloor.ZDiv ZBinary.ZBinAxiomsMod.
  Definition div := Zdiv.
  Definition modulo := Zmod.
  Local Obligation Tactic := simpl_relation.
@@ -314,14 +316,10 @@ Module ZDiv <: ZDivFloor.ZDiv ZBinary.ZBinAxiomsMod.
  Definition mod_pos_bound : forall a b:Z, 0<b -> 0<=a mod b<b.
  Proof. intros; apply Z_mod_lt; auto with zarith. Qed.
  Definition mod_neg_bound := Z_mod_neg.
-End ZDiv.
-
-Module ZDivMod := ZBinary.ZBinAxiomsMod <+ ZDiv.
-
-(** We hence benefit from generic results about this abstract division. *)
 
-Module Z := ZDivFloor.ZDivPropFunct ZDivMod ZBinary.ZBinPropMod.
+ Include ZBinary.Z (* ideally: Zminmax.Z *) <+ ZDivFloor.ZDivPropFunct.
 
+End Z.
 
 (** Existence theorem *)
 
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 53c40ae7d..84303a326 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -9,12 +9,12 @@
 
 (** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
 
-Require Export BinInt Zorder Zminmax.
+Require Export BinInt Zcompare Zorder Zminmax.
 
 Open Local Scope Z_scope.
 
-(** [Zmax] is now [Zminmax.Zmax]. Code that do things like
-  [unfold Zmin.Zmin] will have to be adapted, and neither
+(** [Zmax] is now [BinInt.Zmax]. Code that do things like
+  [unfold Zmax.Zmax] will have to be adapted, and neither
   a [Definition] or a [Notation] here can help much. *)
 
 
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 5dd26fa38..4703faace 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -9,11 +9,11 @@
 
 (** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
 
-Require Import BinInt Zorder Zminmax.
+Require Import BinInt Zcompare Zorder Zminmax.
 
 Open Local Scope Z_scope.
 
-(** [Zmin] is now [Zminmax.Zmin]. Code that do things like
+(** [Zmin] is now [BinInt.Zmin]. Code that do things like
   [unfold Zmin.Zmin] will have to be adapted, and neither
   a [Definition] or a [Notation] here can help much. *)
 
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index c1657e298..70f72568f 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -6,69 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Orders BinInt Zcompare Zorder ZOrderedType
- GenericMinMax.
+Require Import Orders BinInt Zcompare Zorder ZBinary.
 
 (** * Maximum and Minimum of two [Z] numbers *)
 
 Local Open Scope Z_scope.
 
-Unboxed Definition Zmax (n m:Z) :=
-  match n ?= m with
-    | Eq | Gt => n
-    | Lt => m
-  end.
-
-Unboxed Definition Zmin (n m:Z) :=
-  match n ?= m with
-    | Eq | Lt => n
-    | Gt => m
-  end.
-
-(** The functions [Zmax] and [Zmin] implement indeed
-    a maximum and a minimum *)
-
-Lemma Zmax_l : forall x y, y<=x -> Zmax x y = x.
-Proof.
- unfold Zle, Zmax. intros x y. rewrite <- (Zcompare_antisym x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmax_r : forall x y, x<=y -> Zmax x y = y.
-Proof.
- unfold Zle, Zmax. intros x y. generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmin_l : forall x y, x<=y -> Zmin x y = x.
-Proof.
- unfold Zle, Zmin. intros x y. generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmin_r : forall x y, y<=x -> Zmin x y = y.
-Proof.
- unfold Zle, Zmin. intros x y.
- rewrite <- (Zcompare_antisym x y). generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Module ZHasMinMax <: HasMinMax Z_as_OT.
- Definition max := Zmax.
- Definition min := Zmin.
- Definition max_l := Zmax_l.
- Definition max_r := Zmax_r.
- Definition min_l := Zmin_l.
- Definition min_r := Zmin_r.
-End ZHasMinMax.
+(* All generic properties about max and min are already in [ZBinary.Z].
+   We prove here in addition some results specific to Z.
+*)
 
 Module Z.
-
-(** We obtain hence all the generic properties of max and min. *)
-
-Include UsualMinMaxProperties Z_as_OT ZHasMinMax.
-
-(** * Properties specific to the [Z] domain *)
+Include ZBinary.Z.
 
 (** Compatibilities (consequences of monotonicity) *)
 
@@ -177,7 +126,6 @@ Qed.
 
 End Z.
 
-
 (** * Characterization of Pminus in term of Zminus and Zmax *)
 
 Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 3efa70552..59994e32f 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -29,4 +29,3 @@ Zpower.vo
 Zpow_facts.vo
 Zsqrt.vo
 Zwf.vo
-ZOrderedType.vo