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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index f95dcc76f8..647ab0ac05 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.