An update of theories/Numbers

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

11 files changed, 279 insertions, 115 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index 7eed9a8ee..322d36cd3 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -153,34 +153,35 @@ Theorem Zleft_induction :
         forall n : Z, n <= z -> A n.
 Proof NZleft_induction.
 
-Theorem Zorder_induction :
+Theorem Zright_induction' :
   forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z, A z ->
+    forall z : Z,
+      (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
-      (forall n : Z, n < z -> A (S n) -> A n) ->
         forall n : Z, A n.
-Proof NZorder_induction.
+Proof NZright_induction'.
 
-Theorem Zorder_induction' :
+Theorem Zleft_induction' :
   forall A : Z -> Prop, predicate_wd Zeq 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)) ->
-        forall n : Z, A n.
-Proof.
-intros A A_wd z Az AS AP n; apply Zorder_induction with (z := z); try assumption.
-intros m H1 H2. apply AP in H2; [| now apply -> Zlt_le_succ].
-unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m);
-[assumption | apply Zpred_succ].
-Qed.
+    forall z : Z,
+    (forall n : NZ, z <= n -> A n) ->
+    (forall n : Z, n < z -> A (S n) -> A n) ->
+      forall n : NZ, A n.
+Proof NZleft_induction'.
 
-Theorem Zright_induction' :
+Theorem Zstrong_right_induction :
   forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z,
-      (forall n : Z, n <= z -> A n) ->
-      (forall n : Z, z <= n -> A n -> A (S n)) ->
-        forall n : Z, A n.
-Proof NZright_induction'.
+    (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 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 ->
@@ -190,27 +191,71 @@ Theorem Zstrong_right_induction' :
         forall n : Z, A n.
 Proof NZstrong_right_induction'.
 
+Theorem Zstrong_left_induction' :
+  forall A : Z -> Prop, predicate_wd Zeq 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) ->
+      forall n : Z, A n.
+Proof NZstrong_left_induction'.
+
+Theorem Zorder_induction :
+  forall A : Z -> Prop, predicate_wd Zeq 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) ->
+      forall n : Z, A n.
+Proof NZorder_induction.
+
+Theorem Zorder_induction' :
+  forall A : Z -> Prop, predicate_wd Zeq 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)) ->
+      forall n : Z, A n.
+Proof NZorder_induction'.
+
+Theorem Zorder_induction_0 :
+  forall A : Z -> Prop, predicate_wd Zeq A ->
+    A 0 ->
+    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
+    (forall n : Z, n < 0 -> A (S n) -> A n) ->
+      forall n : Z, A n.
+Proof NZorder_induction_0.
+
+Theorem Zorder_induction'_0 :
+  forall A : Z -> Prop, predicate_wd Zeq A ->
+    A 0 ->
+    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
+    (forall n : Z, n <= 0 -> A n -> A (P n)) ->
+      forall n : Z, A n.
+Proof NZorder_induction'_0.
+
+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 n : Z,
-      A (S n) ->
-      (forall m : Z, n < m -> A m -> A (S m)) ->
-        forall m : Z, n < m -> A m.
+    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.
 
 (** Elimintation principle for <= *)
 
 Theorem Zle_ind :
   forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall n : Z,
-      A n ->
-      (forall m : Z, n <= m -> A m -> A (S m)) ->
-        forall m : Z, n <= m -> A m.
+    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.
 
-Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction with (z := 0)).
+(** Well-founded relations *)
+
+Theorem Zlt_wf : forall z : Z, well_founded (fun n m : Z => z <= n /\ n < m).
+Proof NZlt_wf.
+
+Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z).
+Proof NZgt_wf.
 
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index f4c39934f..c0ad96de3 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -400,6 +400,26 @@ Proof.
 intros Az RS; apply NZstrong_right_induction; now apply NZrs_rs'.
 Qed.
 
+Theorem NZright_induction' :
+  (forall n : NZ, n <= z -> A n) -> right_step -> forall n : NZ, A n.
+Proof.
+intros L R n.
+destruct (NZlt_trichotomy n z) as [H | [H | H]].
+apply L; now le_less.
+apply L; now le_equal.
+apply NZright_induction. apply L; now le_equal. assumption. now le_less.
+Qed.
+
+Theorem NZstrong_right_induction' :
+  (forall n : NZ, n <= z -> A n) -> right_step' -> forall n : NZ, A n.
+Proof.
+intros L R n.
+destruct (NZlt_trichotomy n z) as [H | [H | H]].
+apply L; now le_less.
+apply L; now le_equal.
+apply NZstrong_right_induction. assumption. now le_less.
+Qed.
+
 End RightInduction.
 
 Section LeftInduction.
@@ -447,6 +467,26 @@ Proof.
 intros Az LS; apply NZstrong_left_induction; now apply NZls_ls'.
 Qed.
 
+Theorem NZleft_induction' :
+  (forall n : NZ, z <= n -> A n) -> left_step -> forall n : NZ, A n.
+Proof.
+intros R L n.
+destruct (NZlt_trichotomy n z) as [H | [H | H]].
+apply NZleft_induction. apply R. now le_equal. assumption. now le_less.
+rewrite H; apply R; le_equal.
+apply R; le_less.
+Qed.
+
+Theorem NZstrong_left_induction' :
+  (forall n : NZ, z <= n -> A n) -> left_step' -> forall n : NZ, A n.
+Proof.
+intros R L n.
+destruct (NZlt_trichotomy n z) as [H | [H | H]].
+apply NZstrong_left_induction; auto. le_less.
+rewrite H; apply R; le_equal.
+apply R; le_less.
+Qed.
+
 End LeftInduction.
 
 Theorem NZorder_induction :
@@ -462,28 +502,16 @@ now rewrite H.
 now apply NZright_induction; [| | le_less].
 Qed.
 
-Theorem NZright_induction' :
-  (forall n : NZ, n <= z -> A n) ->
+Theorem NZorder_induction' :
+  A z ->
   (forall n : NZ, z <= n -> A n -> A (S n)) ->
+  (forall n : NZ, n <= z -> A n -> A (P n)) ->
     forall n : NZ, A n.
 Proof.
-intros L R n.
-destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply L; now le_less.
-apply L; now le_equal.
-apply NZright_induction. apply L; now le_equal. assumption. now le_less.
-Qed.
-
-Theorem NZstrong_right_induction' :
-  (forall n : NZ, n <= z -> A n) ->
-  (forall n : NZ, z <= n -> (forall m : NZ, z <= m -> m < n -> A m) -> A n) ->
-    forall n : NZ, A n.
-Proof.
-intros L R n.
-destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply L; now le_less.
-apply L; now le_equal.
-apply NZstrong_right_induction. assumption. now le_less.
+intros Az AS AP n; apply NZorder_induction; try assumption.
+intros m H1 H2. apply AP in H2; [| now apply -> NZlt_le_succ].
+unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m);
+[assumption | apply NZpred_succ].
 Qed.
 
 End Center.
@@ -495,6 +523,13 @@ Theorem NZorder_induction_0 :
     forall n : NZ, A n.
 Proof (NZorder_induction 0).
 
+Theorem NZorder_induction'_0 :
+  A 0 ->
+  (forall n : NZ, 0 <= n -> A n -> A (S n)) ->
+  (forall n : NZ, n <= 0 -> A n -> A (P n)) ->
+    forall n : NZ, A n.
+Proof (NZorder_induction' 0).
+
 (** Elimintation principle for < *)
 
 Theorem NZlt_ind : forall (n : NZ),
@@ -530,21 +565,34 @@ Section WF.
 
 Variable z : NZ.
 
-Let R (n m : NZ) := z <= n /\ n < m.
+Let Rlt (n m : NZ) := z <= n /\ n < m.
+Let Rgt (n m : NZ) := m < n /\ n <= z.
+
+Add Morphism Rlt with signature NZeq ==> NZeq ==> iff as Rlt_wd.
+Proof.
+intros x1 x2 H1 x3 x4 H2; unfold Rlt; rewrite H1; now rewrite H2.
+Qed.
 
-Add Morphism R with signature NZeq ==> NZeq ==> iff as R_wd.
+Add Morphism Rgt with signature NZeq ==> NZeq ==> iff as Rgt_wd.
 Proof.
-intros x1 x2 H1 x3 x4 H2; unfold R; rewrite H1; now rewrite H2.
+intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2.
 Qed.
 
-Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc R).
+Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc Rlt).
 Proof.
 unfold predicate_wd, fun_wd.
 intros x1 x2 H; split; intro H1; destruct H1 as [H2];
 constructor; intros; apply H2; now (rewrite H || rewrite <- H).
 Qed.
 
-Theorem NZlt_wf : well_founded R.
+Lemma NZAcc_gt_wd : predicate_wd NZeq (Acc Rgt).
+Proof.
+unfold predicate_wd, fun_wd.
+intros x1 x2 H; split; intro H1; destruct H1 as [H2];
+constructor; intros; apply H2; now (rewrite H || rewrite <- H).
+Qed.
+
+Theorem NZlt_wf : well_founded Rlt.
 Proof.
 unfold well_founded.
 apply NZstrong_right_induction' with (z := z).
@@ -554,6 +602,17 @@ apply <- NZnle_gt in H2. elim H2. now apply NZle_trans with z.
 intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
 Qed.
 
+Theorem NZgt_wf : well_founded Rgt.
+Proof.
+unfold well_founded.
+apply NZstrong_left_induction' with (z := z).
+apply NZAcc_gt_wd.
+intros n H; constructor; intros y [H1 H2].
+apply <- NZnle_gt in H2. elim H2. now apply NZle_lt_trans with n.
+intros n H1 H2; constructor; intros m [H3 H4].
+apply H2. assumption. now apply -> NZlt_le_succ.
+Qed.
+
 End WF.
 
 End NZOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 2a17754d5..052a18c3e 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -15,6 +15,8 @@ Notation P := NZpred.
 Notation plus := NZplus.
 Notation times := NZtimes.
 Notation minus := NZminus.
+Notation lt := NZlt.
+Notation le := NZle.
 Notation "x == y"  := (NZeq x y) (at level 70) : NatScope.
 Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatScope.
 Notation "0" := NZ0 : NatScope.
@@ -36,7 +38,7 @@ Axiom pred_0 : P 0 == 0.
 
 Axiom recursion_wd : forall (A : Set) (Aeq : relation A),
   forall a a' : A, Aeq a a' ->
-    forall f f' : N -> A -> A, eq_fun2 Neq Aeq Aeq f f' ->
+    forall f f' : N -> A -> A, fun2_eq Neq Aeq Aeq f f' ->
       forall x x' : N, x == x' ->
         Aeq (recursion a f x) (recursion a' f' x').
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index c0c479dc8..7c4464632 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -59,7 +59,7 @@ Definition if_zero (A : Set) (a b : A) (n : N) : A :=
 Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
-reflexivity. unfold eq_fun2; now intros. assumption.
+reflexivity. unfold fun2_eq; now intros. assumption.
 Qed.
 
 Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a.
@@ -198,7 +198,7 @@ End PairInduction.
 Section TwoDimensionalInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd Neq Neq R.
+Hypothesis R_wd : relation_wd Neq Neq R.
 
 Add Morphism R with signature Neq ==> Neq ==> iff as R_morph.
 Proof.
@@ -223,12 +223,12 @@ End TwoDimensionalInduction.
   try intros until n;
   try intros until m;
   pattern n, m; apply two_dim_induction; clear n m;
-  [solve_rel_wd | | | ].*)
+  [solve_relation_wd | | | ].*)
 
 Section DoubleInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd Neq Neq R.
+Hypothesis R_wd : relation_wd Neq Neq R.
 
 Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1.
 Proof.
@@ -250,7 +250,7 @@ Ltac double_induct n m :=
   try intros until n;
   try intros until m;
   pattern n, m; apply double_induction; clear n m;
-  [solve_rel_wd | | | ].
+  [solve_relation_wd | | | ].
 
 End NBasePropFunct.
 
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index b792beefe..35e93bbc7 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -26,7 +26,7 @@ unfold natural_isomorphism.
 intros n m Eqxy.
 apply NAxiomsMod1.recursion_wd with (Aeq := Eq2).
 reflexivity.
-unfold eq_fun2. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
+unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
 assumption.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index 5ac1f70fb..fe0ec4e62 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -41,7 +41,7 @@ Qed.
 Theorem minus_gt : forall n m : N, n > m -> n - m ~= 0.
 Proof.
 intros n m H; elim H using lt_ind_rel; clear n m H.
-solve_rel_wd.
+solve_relation_wd.
 intro; rewrite minus_0_r; apply neq_succ_0.
 intros; now rewrite minus_succ.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 3e338825e..8f68716bb 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -163,14 +163,6 @@ Theorem left_induction :
         forall n : N, n <= z -> A n.
 Proof NZleft_induction.
 
-Theorem order_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
-    forall z : N, A z ->
-      (forall n : N, z <= n -> A n -> A (S n)) ->
-      (forall n : N, n < z  -> A (S n) -> A n) ->
-        forall n : N, A n.
-Proof NZorder_induction.
-
 Theorem right_induction' :
   forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N,
@@ -179,6 +171,28 @@ Theorem right_induction' :
         forall n : N, A n.
 Proof NZright_induction'.
 
+Theorem left_induction' :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N,
+    (forall n : NZ, z <= n -> A n) ->
+    (forall n : N, n < z -> A (S n) -> A n) ->
+      forall n : NZ, A n.
+Proof NZleft_induction'.
+
+Theorem strong_right_induction :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N,
+    (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
+       forall n : N, z <= n -> A n.
+Proof NZstrong_right_induction.
+
+Theorem strong_left_induction :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N,
+      (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
+        forall n : N, n <= z -> A n.
+Proof NZstrong_left_induction.
+
 Theorem strong_right_induction' :
   forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N,
@@ -187,6 +201,33 @@ Theorem strong_right_induction' :
         forall n : N, A n.
 Proof NZstrong_right_induction'.
 
+Theorem strong_left_induction' :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N,
+    (forall n : N, z <= n -> A n) ->
+    (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
+      forall n : N, A n.
+Proof NZstrong_left_induction'.
+
+Theorem order_induction :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N, A z ->
+      (forall n : N, z <= n -> A n -> A (S n)) ->
+      (forall n : N, n < z  -> A (S n) -> A n) ->
+        forall n : N, A n.
+Proof NZorder_induction.
+
+Theorem order_induction' :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N, A z ->
+      (forall n : N, z <= n -> A n -> A (S n)) ->
+      (forall n : N, n <= z -> A n -> A (P n)) ->
+        forall n : N, A n.
+Proof NZorder_induction'.
+
+(* We don't need order_induction_0 and order_induction'_0 (see NZOrder and
+ZOrder) since they boil down to regular induction *)
+
 (** Elimintation principle for < *)
 
 Theorem lt_ind :
@@ -207,6 +248,24 @@ Theorem le_ind :
         forall m : N, n <= m -> A m.
 Proof NZle_ind.
 
+(** Well-founded relations *)
+
+Theorem lt_wf : forall z : N, well_founded (fun n m : N => z <= n /\ n < m).
+Proof NZlt_wf.
+
+Theorem gt_wf : forall z : N, well_founded (fun n m : N => m < n /\ n <= z).
+Proof NZgt_wf.
+
+Theorem lt_wf_0 : well_founded lt.
+Proof.
+assert (H : relations_eq lt (fun n m : N => 0 <= n /\ n < m)).
+intros x y; split.
+intro H; split; [apply le_0_l | assumption]. now intros [_ H].
+rewrite H; apply lt_wf.
+(* does not work:
+setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*)
+Qed.
+
 (** Theorems that are true for natural numbers but not for integers *)
 
 (* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)
@@ -247,18 +306,6 @@ split; intro H; [now elim H | intro; now apply lt_irrefl with 0].
 intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
 Qed.
 
-Lemma Acc_nonneg_lt : forall n : N,
-  Acc (fun n m => 0 <= n /\ n < m) n -> Acc NZlt n.
-Proof.
-intros n H; induction H as [n _ H2];
-constructor; intros y H; apply H2; split; [apply le_0_l | assumption].
-Qed.
-
-Theorem lt_wf : well_founded NZlt.
-Proof.
-unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf.
-Qed.
-
 (** Elimination principlies for < and <= for relations *)
 
 Section RelElim.
@@ -266,7 +313,7 @@ Section RelElim.
 (* FIXME: Variable R : relation N. -- does not work *)
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd Neq Neq R.
+Hypothesis R_wd : relation_wd Neq Neq R.
 
 Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.
 Proof R_wd.
@@ -359,7 +406,7 @@ Qed.
 Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *)
 Proof.
 intros n m H; elim H using le_ind_rel.
-solve_rel_wd.
+solve_relation_wd.
 intro; rewrite pred_0; apply le_0_l.
 intros p q H1 _; now do 2 rewrite pred_succ.
 Qed.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index b35af2e01..abd98ebef 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -137,11 +137,11 @@ Qed.
 Theorem recursion_wd :
 forall (A : Set) (Aeq : relation A),
   forall a a' : A, Aeq a a' ->
-    forall f f' : N -> A -> A, eq_fun2 NZeq Aeq Aeq f f' ->
+    forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' ->
       forall x x' : N, x = x' ->
         Aeq (recursion a f x) (recursion a' f' x').
 Proof.
-unfold fun2_wd, NZeq, eq_fun2.
+unfold fun2_wd, NZeq, fun2_eq.
 intros A Aeq a a' Eaa' f f' Eff'.
 intro x; pattern x; apply Nind.
 intros x' H; now rewrite <- H.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index a3109fc6d..0a59ab520 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -145,11 +145,11 @@ Qed.
 
 Theorem recursion_wd : forall (A : Set) (Aeq : relation A),
   forall a a' : A, Aeq a a' ->
-    forall f f' : nat -> A -> A, eq_fun2 (@eq nat) Aeq Aeq f f' ->
+    forall f f' : nat -> A -> A, fun2_eq (@eq nat) Aeq Aeq f f' ->
       forall n n' : nat, n = n' ->
         Aeq (recursion a f n) (recursion a' f' n').
 Proof.
-unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
+unfold fun2_eq; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
 Qed.
 
 Theorem recursion_0 :
@@ -163,7 +163,7 @@ Theorem recursion_succ :
     Aeq a a -> fun2_wd (@eq nat) Aeq Aeq f ->
       forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 Proof.
-unfold eq_fun2; induction n; simpl; auto.
+induction n; simpl; auto.
 Qed.
 
 End NPeanoAxiomsMod.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 5f945701f..5505efd49 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -6,6 +6,7 @@ Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2,
 then it needs to know about bool and have a notation ||. *)
 Require Export QRewrite.
 
+Set Implicit Arguments.
 (*
 Contents:
 - Coercion from bool to Prop
@@ -102,30 +103,51 @@ Definition fun_wd (f : A -> B) := forall x y : A, Aeq x y -> Beq (f x) (f y).
 Definition fun2_wd (f : A -> B -> C) :=
   forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f x' y').
 
-Definition eq_fun : relation (A -> B) :=
+Definition fun_eq : relation (A -> B) :=
   fun f f' => forall x x' : A, Aeq x x' -> Beq (f x) (f' x').
 
-(* Note that reflexivity of eq_fun means that every function
+(* Note that reflexivity of fun_eq means that every function
 is well-defined w.r.t. Aeq and Beq, i.e.,
 forall x x' : A, Aeq x x' -> Beq (f x) (f x') *)
 
-Definition eq_fun2 (f f' : A -> B -> C) :=
+Definition fun2_eq (f f' : A -> B -> C) :=
   forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f' x' y').
 
 End ExtensionalProperties.
 
-Implicit Arguments fun_wd [A B].
-Implicit Arguments fun2_wd [A B C].
-Implicit Arguments eq_fun [A B].
-Implicit Arguments eq_fun2 [A B C].
+(* The following definitions instantiate Beq or Ceq to iff; therefore, they
+have to be outside the ExtensionalProperties section *)
 
 Definition predicate_wd (A : Type) (Aeq : relation A) := fun_wd Aeq iff.
 
-Definition rel_wd (A B : Type) (Aeq : relation A) (Beq : relation B) :=
+Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) :=
   fun2_wd Aeq Beq iff.
 
-Implicit Arguments predicate_wd [A].
-Implicit Arguments rel_wd [A B].
+Definition relations_eq (A B : Type) (R1 R2 : A -> B -> Prop) :=
+  forall (x : A) (y : B), R1 x y <-> R2 x y.
+
+Theorem relations_eq_equiv :
+  forall (A B : Type), equiv (A -> B -> Prop) (@relations_eq A B).
+Proof.
+intros A B; unfold equiv. split; [| split];
+unfold reflexive, symmetric, transitive, relations_eq.
+reflexivity.
+intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
+now symmetry.
+Qed.
+
+Add Relation (fun A B : Type => A -> B -> Prop) relations_eq
+  reflexivity proved by (fun A B : Type => proj1 (relations_eq_equiv A B))
+  symmetry proved by (fun A B : Type => proj2 (proj2 (relations_eq_equiv A B)))
+  transitivity proved by (fun A B : Type => proj1 (proj2 (relations_eq_equiv A B)))
+as relations_eq_rel.
+
+Add Morphism well_founded with signature relations_eq ==> iff as well_founded_wd.
+Proof.
+unfold relations_eq, well_founded; intros A R1 R2 H;
+split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
+intros y H4; apply H3; [now apply <- H | now apply -> H].
+Qed.
 
 Ltac solve_predicate_wd :=
 unfold predicate_wd;
@@ -134,8 +156,8 @@ let y := fresh "y" in
 let H := fresh "H" in
   intros x y H; qiff x y H.
 
-Ltac solve_rel_wd :=
-unfold rel_wd, fun2_wd;
+Ltac solve_relation_wd :=
+unfold relation_wd, fun2_wd;
 let x1 := fresh "x" in
 let y1 := fresh "y" in
 let H1 := fresh "H" in
@@ -145,7 +167,7 @@ let H2 := fresh "H" in
   intros x1 y1 H1 x2 y2 H2;
   qsetoid_rewrite H1;
   qiff x2 y2 H2.
-(* The tactic solve_rel_wd is not very efficient because qsetoid_rewrite
+(* The tactic solve_relation_wd is not very efficient because qsetoid_rewrite
 uses qiff to take the formula apart in order to make it quantifier-free,
 and then qiff is called again and takes the formula apart for the second
 time. It is better to analyze the formula once and generalize qiff to take
@@ -296,21 +318,15 @@ Qed.
 
 Definition LE_Set : forall A : Set, relation A := (@eq).
 
-Lemma eq_equiv : forall A : Set, equiv A (LE_Set A).
+Lemma eq_equiv : forall A : Set, equiv A (@LE_Set A).
 Proof.
 intro A; unfold equiv, LE_Set, reflexive, symmetric, transitive.
 repeat split; [exact (@trans_eq A) | exact (@sym_eq A)].
 (* It is interesting how the tactic split proves reflexivity *)
 Qed.
 
-Add Relation (fun A : Set => A) LE_Set
+(*Add Relation (fun A : Set => A) LE_Set
  reflexivity proved by (fun A : Set => (proj1 (eq_equiv A)))
  symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A))))
  transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A))))
-as EA_rel.
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
+as EA_rel.*)
diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v
index e41052f95..439fc6847 100644
--- a/theories/Numbers/QRewrite.v
+++ b/theories/Numbers/QRewrite.v
@@ -181,8 +181,3 @@ end.
 
 ra (eqcons H0 (eqcons H1 eqnil)).*)
 
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)