4 files changed, 24 insertions, 36 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index 917e3fc123..5f68b2bb15 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -350,9 +350,7 @@ Qed.
 Section PosNeg.
 
 Variable P : Z -> Prop.
-Hypothesis P_wd : predicate_wd Zeq P.
-
-Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed.
+Hypothesis P_wd : Proper (Zeq ==> iff) P.
 
 Theorem Z0_pos_neg :
   P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 7b3c0ba6e8..00e34a5b55 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -64,7 +64,7 @@ Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m.
 Proof NZeq_dne.
 
 Theorem Zcentral_induction :
-forall A : Z -> Prop, predicate_wd Zeq A ->
+forall A : Z -> Prop, Proper (Zeq==>iff) A ->
   forall z : Z, A z ->
     (forall n : Z, A n <-> A (S n)) ->
       forall n : Z, A n.
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 4d927cb3b6..500dd9f535 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -10,22 +10,17 @@
 
 (*i $Id$ i*)
 
+Require Import Bool.
 Require Export NumPrelude.
 
 Module Type ZDomainSignature.
 
 Parameter Inline Z : Set.
 Parameter Inline Zeq : Z -> Z -> Prop.
-Parameter Inline e : Z -> Z -> bool.
+Parameter Inline Zeqb : Z -> Z -> bool.
 
-Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y.
-Axiom eq_equiv : equiv Z Zeq.
-
-Add Relation Z Zeq
- reflexivity proved by (proj1 eq_equiv)
- symmetry proved by (proj2 (proj2 eq_equiv))
- transitivity proved by (proj1 (proj2 eq_equiv))
-as eq_rel.
+Axiom eqb_equiv_eq : forall x y : Z, Zeqb x y = true <-> Zeq x y.
+Instance eq_equiv : Equivalence Zeq.
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
@@ -37,16 +32,11 @@ End ZDomainSignature.
 Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
 Open Local Scope IntScope.
 
-Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
+Instance Zeqb_wd : Proper (Zeq ==> Zeq ==> eq) Zeqb.
 Proof.
 intros x x' Exx' y y' Eyy'.
-case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
-assert (x == y); [apply <- eq_equiv_e; now rewrite H2 |
-assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
-rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]].
-assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 |
-assert (x == y); [rewrite Exx'; now rewrite Eyy' |
-rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
+apply eq_true_iff_eq.
+rewrite 2 eqb_equiv_eq, Exx', Eyy'; auto with *.
 Qed.
 
 Theorem neq_sym : forall n m, n # m -> m # n.
@@ -62,7 +52,7 @@ Qed.
 Declare Left Step ZE_stepl.
 
 (* The right step lemma is just transitivity of Zeq *)
-Declare Right Step (proj1 (proj2 eq_equiv)).
+Declare Right Step (@Equivalence_Transitive _ _ eq_equiv).
 
 End ZDomainProperties.
 
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 1b8bdda408..efd1f0da39 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -221,21 +221,21 @@ Proof NZneq_succ_iter_l.
 in the induction step *)
 
 Theorem Zright_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
         forall n : Z, z <= n -> A n.
 Proof NZright_induction.
 
 Theorem Zleft_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
       (forall n : Z, n < z -> A (S n) -> A n) ->
         forall n : Z, n <= z -> A n.
 Proof NZleft_induction.
 
 Theorem Zright_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
@@ -243,7 +243,7 @@ Theorem Zright_induction' :
 Proof NZright_induction'.
 
 Theorem Zleft_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> A n) ->
     (forall n : Z, n < z -> A (S n) -> A n) ->
@@ -251,21 +251,21 @@ Theorem Zleft_induction' :
 Proof NZleft_induction'.
 
 Theorem Zstrong_right_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
        forall n : Z, z <= n -> A n.
 Proof NZstrong_right_induction.
 
 Theorem Zstrong_left_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
         forall n : Z, n <= z -> A n.
 Proof NZstrong_left_induction.
 
 Theorem Zstrong_right_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
@@ -273,7 +273,7 @@ Theorem Zstrong_right_induction' :
 Proof NZstrong_right_induction'.
 
 Theorem Zstrong_left_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> A n) ->
     (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
@@ -281,7 +281,7 @@ Theorem Zstrong_left_induction' :
 Proof NZstrong_left_induction'.
 
 Theorem Zorder_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
     (forall n : Z, z <= n -> A n -> A (S n)) ->
     (forall n : Z, n < z -> A (S n) -> A n) ->
@@ -289,7 +289,7 @@ Theorem Zorder_induction :
 Proof NZorder_induction.
 
 Theorem Zorder_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
     (forall n : Z, z <= n -> A n -> A (S n)) ->
     (forall n : Z, n <= z -> A n -> A (P n)) ->
@@ -297,7 +297,7 @@ Theorem Zorder_induction' :
 Proof NZorder_induction'.
 
 Theorem Zorder_induction_0 :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     A 0 ->
     (forall n : Z, 0 <= n -> A n -> A (S n)) ->
     (forall n : Z, n < 0 -> A (S n) -> A n) ->
@@ -305,7 +305,7 @@ Theorem Zorder_induction_0 :
 Proof NZorder_induction_0.
 
 Theorem Zorder_induction'_0 :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     A 0 ->
     (forall n : Z, 0 <= n -> A n -> A (S n)) ->
     (forall n : Z, n <= 0 -> A n -> A (P n)) ->
@@ -317,7 +317,7 @@ Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0).
 (** Elimintation principle for < *)
 
 Theorem Zlt_ind :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall n : Z, A (S n) ->
       (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m.
 Proof NZlt_ind.
@@ -325,7 +325,7 @@ Proof NZlt_ind.
 (** Elimintation principle for <= *)
 
 Theorem Zle_ind :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall n : Z, A n ->
       (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m.
 Proof NZle_ind.