f_equiv : a clone of f_equal that handles setoid equivalences

 For example, if we know that [f] is a morphism for [E1==>E2==>E],
 then the goal [E (f x y) (f x' y')] will be transformed by [f_equiv]
 into the subgoals [E1 x x'] and [E2 y y'].

 This way, we can remove most of the explicit use of the morphism
 instances in Numbers (lemmas foo_wd for each operator foo).

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

18 files changed, 97 insertions, 182 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index f95dcc76f..647ab0ac0 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -34,7 +34,7 @@ Theorem add_opp_r : forall n m, n + (- m) == n - m.
 Proof.
 nzinduct m.
 now nzsimpl.
-intro m. rewrite opp_succ, sub_succ_r, add_pred_r; now rewrite pred_inj_wd.
+intro m. rewrite opp_succ, sub_succ_r, add_pred_r. now rewrite pred_inj_wd.
 Qed.
 
 Theorem sub_0_l : forall n, 0 - n == - n.
@@ -96,7 +96,7 @@ Theorem opp_involutive : forall n, - (- n) == n.
 Proof.
 nzinduct n.
 now nzsimpl.
-intro n. rewrite opp_succ, opp_pred; now rewrite succ_inj_wd.
+intro n. rewrite opp_succ, opp_pred. now rewrite succ_inj_wd.
 Qed.
 
 Theorem opp_add_distr : forall n m, - (n + m) == - n + (- m).
@@ -120,7 +120,7 @@ Qed.
 
 Theorem opp_inj_wd : forall n m, - n == - m <-> n == m.
 Proof.
-intros n m; split; [apply opp_inj | apply opp_wd].
+intros n m; split; [apply opp_inj | intros; now f_equiv].
 Qed.
 
 Theorem eq_opp_l : forall n m, - n == m <-> n == - m.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 4afc10201..510548527 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -24,7 +24,7 @@ Qed.
 
 Theorem pred_inj_wd : forall n1 n2, P n1 == P n2 <-> n1 == n2.
 Proof.
-intros n1 n2; split; [apply pred_inj | apply pred_wd].
+intros n1 n2; split; [apply pred_inj | intros; now f_equiv].
 Qed.
 
 Lemma succ_m1 : S (-1) == 0.
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 641375a5c..de6619598 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -166,14 +166,14 @@ Proof.
  apply lt_succ_r. rewrite sub_1_r, succ_pred. now apply lt_0_sub.
  apply le_succ_l. rewrite sub_1_r, succ_pred. apply le_sub_le_add_r.
  rewrite <- (add_0_r (2^n)) at 1. now apply add_le_mono_l.
- rewrite <- add_sub_swap, sub_1_r. apply pred_wd.
+ rewrite <- add_sub_swap, sub_1_r. f_equiv.
  apply opp_inj. rewrite opp_add_distr, opp_sub_distr.
  rewrite (add_comm _ l), <- add_assoc.
  rewrite EQ at 1. apply add_cancel_l.
  rewrite <- opp_add_distr.
  rewrite <- (mul_1_l (2^n)) at 2. rewrite <- mul_add_distr_r.
  rewrite <- mul_opp_l.
- apply mul_wd; try reflexivity.
+ f_equiv.
  rewrite !opp_add_distr.
  rewrite <- mul_opp_r.
  rewrite opp_sub_distr, opp_involutive.
@@ -471,8 +471,8 @@ Proof.
    intros m. now rewrite <- H, bits_0.
   clear n Hn. intros n Hn IH a b (Ha,Ha') H.
   rewrite (div_mod a 2), (div_mod b 2) by order'.
-  apply add_wd; [ | now rewrite <- 2 bit0_mod, H].
-  apply mul_wd. reflexivity.
+  f_equiv; [ | now rewrite <- 2 bit0_mod, H].
+  f_equiv.
   apply IH.
   split. apply div_pos; order'.
   apply div_lt_upper_bound. order'. now rewrite <- pow_succ_r.
@@ -543,7 +543,7 @@ Proof.
   exists 0. intros m Hm. rewrite bits_0, Hk by order.
   symmetry; rewrite <- H0. apply Hk; order.
   revert f Hf Hk. apply le_ind with (4:=LE).
-  (* compat : solve_predicat_wd fails here *)
+  (* compat : solve_proper fails here *)
   apply proper_sym_impl_iff. exact eq_sym.
   clear k LE. intros k k' Hk IH f Hf H. apply IH; trivial.
   now setoid_rewrite Hk.
@@ -967,14 +967,10 @@ Proof.
 Qed.
 
 Instance setbit_wd : Proper (eq==>eq==>eq) setbit.
-Proof.
- intros a a' Ha n n' Hn. unfold setbit. now rewrite Ha, Hn.
-Qed.
+Proof. unfold setbit. solve_proper. Qed.
 
 Instance clearbit_wd : Proper (eq==>eq==>eq) clearbit.
-Proof.
- intros a a' Ha n n' Hn. unfold clearbit. now rewrite Ha, Hn.
-Qed.
+Proof. unfold clearbit. solve_proper. Qed.
 
 Lemma pow2_bits_true : forall n, 0<=n -> (2^n).[n] = true.
 Proof.
@@ -1113,7 +1109,7 @@ Qed.
 Definition lnot a := P (-a).
 
 Instance lnot_wd : Proper (eq==>eq) lnot.
-Proof. intros a a' Ha; unfold lnot; now rewrite Ha. Qed.
+Proof. unfold lnot. solve_proper. Qed.
 
 Lemma lnot_spec : forall a n, 0<=n -> (lnot a).[n] = negb a.[n].
 Proof.
@@ -1251,14 +1247,14 @@ Qed.
 Definition ones n := P (1<<n).
 
 Instance ones_wd : Proper (eq==>eq) ones.
-Proof. intros a a' Ha; unfold ones; now rewrite Ha. Qed.
+Proof. unfold ones. solve_proper. Qed.
 
 Lemma ones_equiv : forall n, ones n == P (2^n).
 Proof.
  intros. unfold ones.
  destruct (le_gt_cases 0 n).
  now rewrite shiftl_mul_pow2, mul_1_l.
- apply pred_wd. rewrite pow_neg_r; trivial.
+ f_equiv. rewrite pow_neg_r; trivial.
  rewrite <- shiftr_opp_r. apply shiftr_eq_0_iff. right; split.
  order'. rewrite log2_1. now apply opp_pos_neg.
 Qed.
@@ -1658,7 +1654,7 @@ Proof.
  rewrite <- add3_bits_div2.
  rewrite (add_comm ((a/2)+_)).
  rewrite <- div_add by order'.
- apply div_wd; try easy.
+ f_equiv.
  rewrite <- !div2_div, mul_comm, mul_add_distr_l.
  rewrite (div2_odd a), <- bit0_odd at 1.
  rewrite (div2_odd b), <- bit0_odd at 1.
@@ -1727,7 +1723,7 @@ Proof.
  le_elim Hm.
  rewrite <- (succ_pred m), lt_succ_r in Hm.
  rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial.
- apply testbit_wd; try easy.
+ f_equiv.
  rewrite add_b2z_double_div2, <- IH1. apply add_carry_div2.
  rewrite <- Hm.
  now rewrite add_b2z_double_bit0, add3_bit0, b2z_bit0.
diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v
index f381953fb..052d68ab6 100644
--- a/theories/Numbers/Integer/Abstract/ZLcm.v
+++ b/theories/Numbers/Integer/Abstract/ZLcm.v
@@ -149,7 +149,7 @@ Proof.
  apply mod_divide, div_exact in H; try order.
  rewrite <- H.
  rewrite <- gcd_mul_mono_l_nonneg; try order.
- apply gcd_wd; symmetry; apply div_exact; try order;
+ f_equiv; symmetry; apply div_exact; try order;
   apply mod_divide; trivial; try order.
 Qed.
 
@@ -211,9 +211,7 @@ Qed.
 Definition lcm a b := abs (a*(b/gcd a b)).
 
 Instance lcm_wd : Proper (eq==>eq==>eq) lcm.
-Proof.
- unfold lcm. intros x x' Hx y y' Hy. now rewrite Hx, Hy.
-Qed.
+Proof. unfold lcm. solve_proper. Qed.
 
 Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 ->
   a * (b / gcd a b) == (a*b)/gcd a b.
@@ -270,7 +268,7 @@ Proof.
  exists b'.
  rewrite <- mul_assoc, Hb'.
  rewrite (proj2 (div_exact c g NEQ)).
- rewrite <- Ha', mul_assoc. apply mul_wd; try easy.
+ rewrite <- Ha', mul_assoc. f_equiv.
  apply div_exact; trivial.
  apply mod_divide; trivial.
  apply mod_divide; trivial. transitivity a; trivial.
@@ -423,7 +421,7 @@ Proof.
   nzsimpl. rewrite lcm_0_l. now nzsimpl.
  unfold lcm.
  rewrite gcd_mul_mono_l.
- rewrite !abs_mul, mul_assoc. apply mul_wd; try easy.
+ rewrite !abs_mul, mul_assoc. f_equiv.
  rewrite <- (abs_sgn p) at 1. rewrite <- mul_assoc.
  rewrite div_mul_cancel_l; trivial.
  rewrite divide_div_mul_exact; trivial. rewrite abs_mul.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 6d2fa41fc..c7795ab90 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -174,7 +174,7 @@ le_elim Hn; split; intros m H.
 destruct (lt_1_mul_l n m) as [|[|]]; order'.
 rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'.
 now left.
-intros; right; symmetry; now apply opp_wd.
+intros; right. now f_equiv.
 Qed.
 
 Theorem lt_mul_diag_l : forall n m, n < 0 -> (1 < m <-> n * m < n).
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v
index 5c7e9eb14..b364ec3f0 100644
--- a/theories/Numbers/Integer/Abstract/ZParity.v
+++ b/theories/Numbers/Integer/Abstract/ZParity.v
@@ -28,7 +28,7 @@ Qed.
 Lemma even_opp : forall n, even (-n) = even n.
 Proof.
  assert (H : forall n, Even n -> Even (-n)).
-  intros n (m,H). exists (-m). rewrite mul_opp_r. now apply opp_wd.
+  intros n (m,H). exists (-m). rewrite mul_opp_r. now f_equiv.
  intros. rewrite eq_iff_eq_true, !even_spec.
  split. rewrite <- (opp_involutive n) at 2. apply H.
  apply H.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 2b568dddc..dbcc1961e 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -131,15 +131,14 @@ Qed.
 
 Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub.
 Proof.
-intros n1 m1 H1 n2 m2 H2. rewrite 2 sub_add_opp.
-apply add_wd, opp_wd; auto.
+intros n1 m1 H1 n2 m2 H2. rewrite 2 sub_add_opp. now do 2 f_equiv.
 Qed.
 
 Lemma mul_comm : forall n m, n*m == m*n.
 Proof.
 intros (n1,n2) (m1,m2); compute.
 rewrite (add_comm (m1*n2)%N).
-apply N.add_wd; apply N.add_wd; apply mul_comm.
+do 2 f_equiv; apply mul_comm.
 Qed.
 
 Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index fdec8ceb7..ee03e5f94 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -157,7 +157,7 @@ Proof.
  intros n m H. apply le_ind with (4:=H). solve_proper.
  exists 0; nzsimpl; split; order.
  clear m H. intros m H (p & EQ & LE). exists (S p).
-  split. nzsimpl. now apply succ_wd. now apply le_le_succ_r.
+  split. nzsimpl. now f_equiv. now apply le_le_succ_r.
 Qed.
 
 (** For the moment, it doesn't seem possible to relate
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 7c7f43de0..56fad9347 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -48,7 +48,7 @@ Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2.
 Proof.
 intros; split.
 apply succ_inj.
-intros. now apply succ_wd.
+intros. now f_equiv.
 Qed.
 
 Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 9c01ba8cd..176e557b8 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -85,7 +85,7 @@ intros n n' Hn. rewrite Hn; auto with *.
 reflexivity.
 split; intros (p & q & H).
 exists p; exists (Datatypes.S q). rewrite <- iter_alt; simpl.
- apply succ_wd; auto.
+ now f_equiv.
 exists (Datatypes.S p); exists q. rewrite iter_alt; auto.
 Qed.
 
@@ -373,14 +373,14 @@ Lemma ofnat_add_l : forall n m, [n]+m == (S^n) m.
 Proof.
  induction n; intros.
  apply add_0_l.
- rewrite ofnat_succ, add_succ_l. simpl; apply succ_wd; auto.
+ rewrite ofnat_succ, add_succ_l. simpl. now f_equiv.
 Qed.
 
 Lemma ofnat_add : forall n m, [n+m] == [n]+[m].
 Proof.
  intros. rewrite ofnat_add_l.
  induction n; simpl. reflexivity.
- rewrite ofnat_succ. now apply succ_wd.
+ rewrite ofnat_succ. now f_equiv.
 Qed.
 
 Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].
@@ -389,14 +389,14 @@ Proof.
  symmetry. apply mul_0_l.
  rewrite plus_comm.
  rewrite ofnat_succ, ofnat_add, mul_succ_l.
- now apply add_wd.
+ now f_equiv.
 Qed.
 
 Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.
 Proof.
  induction m; simpl; intros.
  rewrite ofnat_zero. apply sub_0_r.
- rewrite ofnat_succ, sub_succ_r. now apply pred_wd.
+ rewrite ofnat_succ, sub_succ_r. now f_equiv.
 Qed.
 
 Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 3cd78351d..7061dddcd 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -96,7 +96,7 @@ Qed.
 
 Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof.
-intros n m p Hp; split; intro H; [|now apply mul_wd].
+intros n m p Hp; split; intro H; [|now f_equiv].
 apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp];
  destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.
 apply (mul_lt_mono_neg_l p) in LT; order.
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 4287319e4..29109ccb6 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -33,12 +33,12 @@ Proof. unfold Odd. solve_proper. Qed.
 
 Instance even_wd : Proper (eq==>Logic.eq) even.
 Proof.
- intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now apply Even_wd.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now f_equiv.
 Qed.
 
 Instance odd_wd : Proper (eq==>Logic.eq) odd.
 Proof.
- intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now apply Odd_wd.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now f_equiv.
 Qed.
 
 (** Evenness and oddity are dual notions *)
@@ -141,7 +141,7 @@ Lemma Odd_succ : forall n, Odd (S n) <-> Even n.
 Proof.
  split; intros (m,H).
  exists m. apply succ_inj. now rewrite add_1_r in H.
- exists m. rewrite add_1_r. now apply succ_wd.
+ exists m. rewrite add_1_r. now f_equiv.
 Qed.
 
 Lemma odd_succ : forall n, odd (S n) = even n.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 8b6dcc3d6..6e85c6893 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -323,7 +323,7 @@ Proof.
  intros (b & Hb & H).
  rewrite H. rewrite sqrt_square; try order.
  symmetry.
- rewrite <- (lt_succ_pred 0 b Hb). apply succ_wd.
+ rewrite <- (lt_succ_pred 0 b Hb). f_equiv.
  rewrite <- (lt_succ_pred 0 b²) in H. apply succ_inj in H.
  now rewrite H, sqrt_pred_square.
  now apply mul_pos_pos.
@@ -450,7 +450,7 @@ Proof.
   by (apply le_lt_trans with (P b)²; trivial using square_nonneg).
  rewrite sqrt_up_eqn; trivial.
  assert (Hb' := lt_succ_pred 0 b Hb).
- rewrite <- Hb'. apply succ_wd. apply sqrt_unique.
+ rewrite <- Hb'. f_equiv. apply sqrt_unique.
  rewrite <- le_succ_l, <- lt_succ_r, Hb'.
  rewrite (lt_succ_pred 0 a Ha). now split.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index 70f6f7945..f5b900532 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -39,8 +39,7 @@ Proof.
  intros a b c Hb H.
  apply div_unique with 0.
  generalize (pow_nonzero b c Hb) (le_0_l (b^c)); order'.
- nzsimpl. rewrite <- pow_mul_l. apply pow_wd. now apply div_exact.
- reflexivity.
+ nzsimpl. rewrite <- pow_mul_l. f_equiv. now apply div_exact.
 Qed.
 
 (** An injection from bits [true] and [false] to numbers 1 and 0.
@@ -309,8 +308,8 @@ Proof.
  rewrite EQ in H |- *. symmetry. apply bits_inj_0.
  intros n. now rewrite <- H, bits_0.
  rewrite (div_mod a 2), (div_mod b 2) by order'.
- apply add_wd; [ | now rewrite <- 2 bit0_mod, H].
- apply mul_wd. reflexivity.
+ f_equiv; [ | now rewrite <- 2 bit0_mod, H].
+ f_equiv.
  apply IH; trivial using le_0_l.
  apply div_lt; order'.
  intro n. rewrite 2 div2_bits. apply H.
@@ -697,14 +696,10 @@ Proof.
 Qed.
 
 Instance setbit_wd : Proper (eq==>eq==>eq) setbit.
-Proof.
- intros a a' Ha n n' Hn. unfold setbit. now rewrite Ha, Hn.
-Qed.
+Proof. unfold setbit. solve_proper. Qed.
 
 Instance clearbit_wd : Proper (eq==>eq==>eq) clearbit.
-Proof.
- intros a a' Ha n n' Hn. unfold clearbit. now rewrite Ha, Hn.
-Qed.
+Proof. unfold clearbit. solve_proper. Qed.
 
 Lemma pow2_bits_true : forall n, (2^n).[n] = true.
 Proof.
@@ -853,10 +848,10 @@ Definition ones n := P (1 << n).
 Definition lnot a n := lxor a (ones n).
 
 Instance ones_wd : Proper (eq==>eq) ones.
-Proof. intros a a' Ha; unfold ones; now rewrite Ha. Qed.
+Proof. unfold ones. solve_proper. Qed.
 
 Instance lnot_wd : Proper (eq==>eq==>eq) lnot.
-Proof. intros a a' Ha n n' Hn; unfold lnot; now rewrite Ha, Hn. Qed.
+Proof. unfold lnot. solve_proper. Qed.
 
 Lemma ones_equiv : forall n, ones n == P (2^n).
 Proof.
@@ -1225,7 +1220,7 @@ Proof.
  rewrite <- add3_bits_div2.
  rewrite (add_comm ((a/2)+_)).
  rewrite <- div_add by order'.
- apply div_wd; try easy.
+ f_equiv.
  rewrite <- !div2_div, mul_comm, mul_add_distr_l.
  rewrite (div2_odd a), <- bit0_odd at 1. fold (b2n a.[0]).
  rewrite (div2_odd b), <- bit0_odd at 1. fold (b2n b.[0]).
@@ -1273,7 +1268,7 @@ Proof.
  destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ.
  now rewrite add_b2n_double_bit0, add3_bit0, b2n_bit0.
  rewrite <- !div2_bits, <- 2 lxor_spec.
- apply testbit_wd; try easy.
+ f_equiv.
  rewrite add_b2n_double_div2, <- IH1. apply add_carry_div2.
  (* - carry *)
  rewrite add_b2n_double_div2.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 8df64756a..8df715af9 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -28,8 +28,8 @@ Implicit Arguments if_zero [A].
 Instance if_zero_wd (A : Type) :
  Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).
 Proof.
-intros; unfold if_zero.
-repeat red; intros. apply recursion_wd; auto. repeat red; auto.
+unfold if_zero. (* TODO : solve_proper : SLOW + BUG *)
+f_equiv'.
 Qed.
 
 Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a.
@@ -51,17 +51,9 @@ Definition def_add (x y : N.t) := recursion y (fun _ => S) x.
 
 Local Infix "+++" := def_add (at level 50, left associativity).
 
-Instance def_add_prewd : Proper (N.eq==>N.eq==>N.eq) (fun _ => S).
-Proof.
-intros _ _ _ p p' Epp'; now rewrite Epp'.
-Qed.
-
 Instance def_add_wd : Proper (N.eq ==> N.eq ==> N.eq) def_add.
 Proof.
-intros x x' Exx' y y' Eyy'. unfold def_add.
-(* TODO: why rewrite Exx' don't work here (or verrrry slowly) ? *)
-apply recursion_wd with (Aeq := N.eq); auto with *.
-apply def_add_prewd.
+unfold def_add. f_equiv'.
 Qed.
 
 Theorem def_add_0_l : forall y, 0 +++ y == y.
@@ -72,7 +64,7 @@ Qed.
 Theorem def_add_succ_l : forall x y, S x +++ y == S (x +++ y).
 Proof.
 intros x y; unfold def_add.
-rewrite recursion_succ; auto with *.
+rewrite recursion_succ; f_equiv'.
 Qed.
 
 Theorem def_add_add : forall n m, n +++ m == n + m.
@@ -89,18 +81,10 @@ Definition def_mul (x y : N.t) := recursion 0 (fun _ p => p +++ x) y.
 
 Local Infix "**" := def_mul (at level 40, left associativity).
 
-Instance def_mul_prewd :
- Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun x _ p => p +++ x).
-Proof.
-repeat red; intros; now apply def_add_wd.
-Qed.
-
 Instance def_mul_wd : Proper (N.eq ==> N.eq ==> N.eq) def_mul.
 Proof.
-unfold def_mul.
-intros x x' Exx' y y' Eyy'.
-apply recursion_wd; auto with *.
-now apply def_mul_prewd.
+unfold def_mul. (* TODO : solve_proper SLOW + BUG *)
+f_equiv'.
 Qed.
 
 Theorem def_mul_0_r : forall x, x ** 0 == 0.
@@ -112,7 +96,7 @@ Theorem def_mul_succ_r : forall x y, x ** S y == x ** y +++ x.
 Proof.
 intros x y; unfold def_mul.
 rewrite recursion_succ; auto with *.
-now apply def_mul_prewd.
+f_equiv'.
 Qed.
 
 Theorem def_mul_mul : forall n m, n ** m == n * m.
@@ -133,25 +117,9 @@ recursion
 
 Local Infix "<<" := ltb (at level 70, no associativity).
 
-Instance ltb_prewd1 : Proper (N.eq==>Logic.eq) (if_zero false true).
-Proof.
-red; intros; apply if_zero_wd; auto.
-Qed.
-
-Instance ltb_prewd2 : Proper (N.eq==>(N.eq==>Logic.eq)==>N.eq==>Logic.eq)
- (fun _ f n => recursion false (fun n' _ => f n') n).
-Proof.
-repeat red; intros; simpl.
-apply recursion_wd; auto with *.
-repeat red; auto.
-Qed.
-
 Instance ltb_wd : Proper (N.eq ==> N.eq ==> Logic.eq) ltb.
 Proof.
-unfold ltb.
-intros n n' Hn m m' Hm.
-apply f_equiv; auto with *.
-apply recursion_wd; auto; [ apply ltb_prewd1 | apply ltb_prewd2 ].
+unfold ltb. f_equiv'.
 Qed.
 
 Theorem ltb_base : forall n, 0 << n = if_zero false true n.
@@ -163,11 +131,9 @@ Theorem ltb_step :
   forall m n, S m << n = recursion false (fun n' _ => m << n') n.
 Proof.
 intros m n; unfold ltb at 1.
-apply f_equiv; auto with *.
-rewrite recursion_succ by (apply ltb_prewd1||apply ltb_prewd2).
-fold (ltb m).
-repeat red; intros. apply recursion_wd; auto.
-repeat red; intros; now apply ltb_wd.
+f_equiv.
+rewrite recursion_succ; f_equiv'.
+reflexivity.
 Qed.
 
 (* Above, we rewrite applications of function. Is it possible to rewrite
@@ -189,8 +155,7 @@ Qed.
 Theorem succ_ltb_mono : forall n m, (S n << S m) = (n << m).
 Proof.
 intros n m.
-rewrite ltb_step. rewrite recursion_succ; try reflexivity.
-repeat red; intros; now apply ltb_wd.
+rewrite ltb_step. rewrite recursion_succ; f_equiv'.
 Qed.
 
 Theorem ltb_lt : forall n m, n << m = true <-> n < m.
@@ -215,9 +180,7 @@ Definition even (x : N.t) := recursion true (fun _ p => negb p) x.
 
 Instance even_wd : Proper (N.eq==>Logic.eq) even.
 Proof.
-intros n n' Hn. unfold even.
-apply recursion_wd; auto.
-congruence.
+unfold even. f_equiv'.
 Qed.
 
 Theorem even_0 : even 0 = true.
@@ -229,19 +192,12 @@ Qed.
 Theorem even_succ : forall x, even (S x) = negb (even x).
 Proof.
 unfold even.
-intro x; rewrite recursion_succ; try reflexivity.
-congruence.
+intro x; rewrite recursion_succ; f_equiv'.
 Qed.
 
 (*****************************************************)
 (**                Division by 2                     *)
 
-Local Notation "a <= b <= c" := (a<=b /\ b<=c).
-Local Notation "a <= b < c" := (a<=b /\ b<c).
-Local Notation "a < b <= c" := (a<b /\ b<=c).
-Local Notation "a < b < c" := (a<b /\ b<c).
-Local Notation "2" := (S 1).
-
 Definition half_aux (x : N.t) : N.t * N.t :=
   recursion (0, 0) (fun _ p => let (x1, x2) := p in (S x2, x1)) x.
 
@@ -250,14 +206,14 @@ Definition half (x : N.t) := snd (half_aux x).
 Instance half_aux_wd : Proper (N.eq ==> N.eq*N.eq) half_aux.
 Proof.
 intros x x' Hx. unfold half_aux.
-apply recursion_wd; auto with *.
+f_equiv; trivial.
 intros y y' Hy (u,v) (u',v') (Hu,Hv). compute in *.
 rewrite Hu, Hv; auto with *.
 Qed.
 
 Instance half_wd : Proper (N.eq==>N.eq) half.
 Proof.
-intros x x' Hx. unfold half. rewrite Hx; auto with *.
+unfold half. f_equiv'.
 Qed.
 
 Lemma half_aux_0 : half_aux 0 = (0,0).
@@ -272,8 +228,7 @@ intros.
 remember (half_aux x) as h.
 destruct h as (f,s); simpl in *.
 unfold half_aux in *.
-rewrite recursion_succ, <- Heqh; simpl; auto.
-repeat red; intros; subst; auto.
+rewrite recursion_succ, <- Heqh; simpl; f_equiv'.
 Qed.
 
 Theorem half_aux_spec : forall n,
@@ -285,7 +240,7 @@ rewrite half_aux_0; simpl; rewrite add_0_l; auto with *.
 intros.
 rewrite half_aux_succ. simpl.
 rewrite add_succ_l, add_comm; auto.
-apply succ_wd; auto.
+now f_equiv.
 Qed.
 
 Theorem half_aux_spec2 : forall n,
@@ -298,7 +253,7 @@ rewrite half_aux_0; simpl. auto with *.
 intros.
 rewrite half_aux_succ; simpl.
 destruct H; auto with *.
-right; apply succ_wd; auto with *.
+right; now f_equiv.
 Qed.
 
 Theorem half_0 : half 0 == 0.
@@ -315,7 +270,7 @@ Theorem half_double : forall n,
  n == 2 * half n \/ n == 1 + 2 * half n.
 Proof.
 intros. unfold half.
-nzsimpl.
+nzsimpl'.
 destruct (half_aux_spec2 n) as [H|H]; [left|right].
 rewrite <- H at 1. apply half_aux_spec.
 rewrite <- add_succ_l. rewrite <- H at 1. apply half_aux_spec.
@@ -353,16 +308,16 @@ Qed.
 Theorem half_decrease : forall n, 0 < n -> half n < n.
 Proof.
 intros n LT.
-destruct (half_double n) as [E|E]; rewrite E at 2;
- rewrite ?mul_succ_l, ?mul_0_l, ?add_0_l, ?add_assoc.
+destruct (half_double n) as [E|E]; rewrite E at 2; nzsimpl'.
 rewrite <- add_0_l at 1.
 rewrite <- add_lt_mono_r.
 assert (LE : 0 <= half n) by apply le_0_l.
-nzsimpl. le_elim LE; auto.
+le_elim LE; auto.
 rewrite <- LE, mul_0_r in E. rewrite E in LT. destruct (nlt_0_r _ LT).
+rewrite <- add_succ_l.
 rewrite <- add_0_l at 1.
 rewrite <- add_lt_mono_r.
-nzsimpl. apply lt_0_succ.
+apply lt_0_succ.
 Qed.
 
 
@@ -373,17 +328,9 @@ Definition pow (n m : N.t) := recursion 1 (fun _ r => n*r) m.
 
 Local Infix "^^" := pow (at level 30, right associativity).
 
-Instance pow_prewd :
- Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun n _ r => n*r).
-Proof.
-intros n n' Hn x x' Hx y y' Hy. rewrite Hn, Hy; auto with *.
-Qed.
-
 Instance pow_wd : Proper (N.eq==>N.eq==>N.eq) pow.
 Proof.
-intros n n' Hn m m' Hm. unfold pow.
-apply recursion_wd; auto with *.
-now apply pow_prewd.
+unfold pow. f_equiv'.
 Qed.
 
 Lemma pow_0 : forall n, n^^0 == 1.
@@ -393,8 +340,7 @@ Qed.
 
 Lemma pow_succ : forall n m, n^^(S m) == n*(n^^m).
 Proof.
-intros. unfold pow. rewrite recursion_succ; auto with *.
-now apply pow_prewd.
+intros. unfold pow. rewrite recursion_succ; f_equiv'.
 Qed.
 
 
@@ -415,15 +361,13 @@ Proof.
 intros g g' Hg n n' Hn.
 rewrite Hn.
 destruct (n' << 2); auto with *.
-apply succ_wd.
-apply Hg. rewrite Hn; auto with *.
+f_equiv. apply Hg. now f_equiv.
 Qed.
 
 Instance log_wd : Proper (N.eq==>N.eq) log.
 Proof.
 intros x x' Exx'. unfold log.
-apply strong_rec_wd; auto with *.
-apply log_prewd.
+apply strong_rec_wd; f_equiv'.
 Qed.
 
 Lemma log_good_step : forall n h1 h2,
@@ -434,8 +378,8 @@ Proof.
 intros n h1 h2 E.
 destruct (n<<2) as [ ]_eqn:H.
 auto with *.
-apply succ_wd, E, half_decrease.
-rewrite <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
+f_equiv. apply E, half_decrease.
+rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
 order'.
 Qed.
 Hint Resolve log_good_step.
@@ -469,12 +413,12 @@ destruct (lt_ge_cases k 2) as [LT|LE].
 rewrite log_init, pow_0 by auto.
 rewrite <- le_succ_l, <- one_succ in Hk2.
 le_elim Hk2.
-rewrite <- nle_gt, le_succ_l in LT. destruct LT; auto.
+rewrite two_succ, <- nle_gt, le_succ_l in LT. destruct LT; auto.
 rewrite <- Hk2.
 rewrite half_1; auto using lt_0_1, le_refl.
 (* step *)
 rewrite log_step, pow_succ by auto.
-rewrite le_succ_l in LE.
+rewrite two_succ, le_succ_l in LE.
 destruct (IH (half k)) as (IH1,IH2).
  rewrite <- lt_succ_r. apply lt_le_trans with k; auto.
   now apply half_decrease.
@@ -484,10 +428,10 @@ split.
 rewrite <- le_succ_l in IH1.
 apply mul_le_mono_l with (p:=2) in IH1.
 eapply lt_le_trans; eauto.
-nzsimpl.
+nzsimpl'.
 rewrite lt_succ_r.
 eapply le_trans; [ eapply half_lower_bound | ].
-nzsimpl; apply le_refl.
+nzsimpl'; apply le_refl.
 eapply le_trans; [ | eapply half_upper_bound ].
 apply mul_le_mono_l; auto.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 1fe6ed9bf..bcf746a7d 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -23,11 +23,8 @@ Definition natural_isomorphism : N1.t -> N2.t :=
 Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism.
 Proof.
 unfold natural_isomorphism.
-intros n m Eqxy.
-apply N1.recursion_wd.
-reflexivity.
-intros _ _ _ y' y'' H. now apply N2.succ_wd.
-assumption.
+repeat red; intros. f_equiv; trivial.
+repeat red; intros. now f_equiv.
 Qed.
 
 Theorem natural_isomorphism_0 : natural_isomorphism N1.zero == N2.zero.
@@ -40,7 +37,7 @@ Theorem natural_isomorphism_succ :
 Proof.
 unfold natural_isomorphism.
 intro n. rewrite N1.recursion_succ; auto with *.
-repeat red; intros. apply N2.succ_wd; auto.
+repeat red; intros. now f_equiv.
 Qed.
 
 Theorem hom_nat_iso : homomorphism natural_isomorphism.
diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v
index 8a1a4def6..321508f58 100644
--- a/theories/Numbers/Natural/Abstract/NLcm.v
+++ b/theories/Numbers/Natural/Abstract/NLcm.v
@@ -59,7 +59,7 @@ Proof.
  apply mod_divide, div_exact in H; try order.
  rewrite <- H.
  rewrite <- gcd_mul_mono_l; try order.
- apply gcd_wd; symmetry; apply div_exact; try order;
+ f_equiv; symmetry; apply div_exact; try order;
   apply mod_divide; trivial; try order.
 Qed.
 
@@ -95,9 +95,7 @@ Qed.
 Definition lcm a b := a*(b/gcd a b).
 
 Instance lcm_wd : Proper (eq==>eq==>eq) lcm.
-Proof.
- unfold lcm. intros x x' Hx y y' Hy. now rewrite Hx, Hy.
-Qed.
+Proof. unfold lcm. solve_proper. Qed.
 
 Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 ->
   a * (b / gcd a b) == (a*b)/gcd a b.
@@ -154,7 +152,7 @@ Proof.
  exists b'.
  rewrite <- mul_assoc, Hb'.
  rewrite (proj2 (div_exact c g NEQ)).
- rewrite <- Ha', mul_assoc. apply mul_wd; try easy.
+ rewrite <- Ha', mul_assoc. f_equiv.
  apply div_exact; trivial.
  apply mod_divide; trivial.
  apply mod_divide; trivial. transitivity a; trivial.
@@ -264,7 +262,7 @@ Proof.
   nzsimpl. rewrite lcm_0_l. now nzsimpl.
  unfold lcm.
  rewrite gcd_mul_mono_l.
- rewrite mul_assoc. apply mul_wd; try easy.
+ rewrite mul_assoc. f_equiv.
  now rewrite div_mul_cancel_l.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index a52a52e76..039eefdf5 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -13,6 +13,8 @@ and proves its properties *)
 
 Require Export NSub.
 
+Ltac f_equiv' := repeat progress (f_equiv; try intros ? ? ?; auto).
+
 Module NStrongRecProp (Import N : NAxiomsRecSig').
 Include NSubProp N.
 
@@ -49,30 +51,18 @@ Proof.
 reflexivity.
 Qed.
 
-(** We need a result similar to [f_equal], but for setoid equalities. *)
-Lemma f_equiv : forall f g x y,
- (N.eq==>Aeq)%signature f g -> N.eq x y -> Aeq (f x) (g y).
-Proof.
-auto.
-Qed.
-
 Instance strong_rec0_wd :
  Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> N.eq ==> Aeq)
   strong_rec0.
 Proof.
-unfold strong_rec0.
-repeat red; intros.
-apply f_equiv; auto.
-apply recursion_wd; try red; auto.
+unfold strong_rec0; f_equiv'.
 Qed.
 
 Instance strong_rec_wd :
  Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> Aeq) strong_rec.
 Proof.
 intros a a' Eaa' f f' Eff' n n' Enn'.
-rewrite !strong_rec_alt.
-apply strong_rec0_wd; auto.
-now rewrite Enn'.
+rewrite !strong_rec_alt; f_equiv'.
 Qed.
 
 Section FixPoint.
@@ -90,18 +80,16 @@ Lemma strong_rec0_succ : forall a n m,
  Aeq (strong_rec0 a f (S n) m) (f (strong_rec0 a f n) m).
 Proof.
 intros. unfold strong_rec0.
-apply f_equiv; auto with *.
-rewrite recursion_succ; try (repeat red; auto with *; fail).
-apply f_wd.
-apply recursion_wd; try red; auto with *.
+f_equiv.
+rewrite recursion_succ; f_equiv'.
+reflexivity.
 Qed.
 
 Lemma strong_rec_0 : forall a,
  Aeq (strong_rec a f 0) (f (fun _ => a) 0).
 Proof.
-intros. rewrite strong_rec_alt, strong_rec0_succ.
-apply f_wd; auto with *.
-red; intros; rewrite strong_rec0_0; auto with *.
+intros. rewrite strong_rec_alt, strong_rec0_succ; f_equiv'.
+rewrite strong_rec0_0. reflexivity.
 Qed.
 
 (* We need an assumption saying that for every n, the step function (f h n)
@@ -156,7 +144,7 @@ intros.
 transitivity (f (fun n => strong_rec0 a f (S n) n) n).
 rewrite strong_rec_alt.
 apply strong_rec0_fixpoint.
-apply f_wd; auto with *.
+f_equiv.
 intros x x' Hx; rewrite strong_rec_alt, Hx; auto with *.
 Qed.