1 files changed, 19 insertions, 13 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index 2c386a980c..f95dcc76f8 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -16,23 +16,24 @@ Include ZBaseProp Z.
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
 
+Hint Rewrite opp_0 : nz.
+
 Theorem add_pred_l : forall n m, P n + m == P (n + m).
 Proof.
 intros n m.
 rewrite <- (succ_pred n) at 2.
-rewrite add_succ_l. now rewrite pred_succ.
+now rewrite add_succ_l, pred_succ.
 Qed.
 
 Theorem add_pred_r : forall n m, n + P m == P (n + m).
 Proof.
-intros n m; rewrite (add_comm n (P m)), (add_comm n m);
-apply add_pred_l.
+intros n m; rewrite 2 (add_comm n); apply add_pred_l.
 Qed.
 
 Theorem add_opp_r : forall n m, n + (- m) == n - m.
 Proof.
 nzinduct m.
-rewrite opp_0; rewrite sub_0_r; now rewrite add_0_r.
+now nzsimpl.
 intro m. rewrite opp_succ, sub_succ_r, add_pred_r; now rewrite pred_inj_wd.
 Qed.
 
@@ -43,7 +44,7 @@ Qed.
 
 Theorem sub_succ_l : forall n m, S n - m == S (n - m).
 Proof.
-intros n m; do 2 rewrite <- add_opp_r; now rewrite add_succ_l.
+intros n m; rewrite <- 2 add_opp_r; now rewrite add_succ_l.
 Qed.
 
 Theorem sub_pred_l : forall n m, P n - m == P (n - m).
@@ -67,7 +68,7 @@ Qed.
 Theorem sub_diag : forall n, n - n == 0.
 Proof.
 nzinduct n.
-now rewrite sub_0_r.
+now nzsimpl.
 intro n. rewrite sub_succ_r, sub_succ_l; now rewrite pred_succ.
 Qed.
 
@@ -88,20 +89,20 @@ Qed.
 
 Theorem add_sub_assoc : forall n m p, n + (m - p) == (n + m) - p.
 Proof.
-intros n m p; do 2 rewrite <- add_opp_r; now rewrite add_assoc.
+intros n m p; rewrite <- 2 add_opp_r; now rewrite add_assoc.
 Qed.
 
 Theorem opp_involutive : forall n, - (- n) == n.
 Proof.
 nzinduct n.
-now do 2 rewrite opp_0.
+now nzsimpl.
 intro n. rewrite opp_succ, opp_pred; now rewrite succ_inj_wd.
 Qed.
 
 Theorem opp_add_distr : forall n m, - (n + m) == - n + (- m).
 Proof.
 intros n m; nzinduct n.
-rewrite opp_0; now do 2 rewrite add_0_l.
+now nzsimpl.
 intro n. rewrite add_succ_l; do 2 rewrite opp_succ; rewrite add_pred_l.
 now rewrite pred_inj_wd.
 Qed.
@@ -114,7 +115,7 @@ Qed.
 
 Theorem opp_inj : forall n m, - n == - m -> n == m.
 Proof.
-intros n m H. apply opp_wd in H. now do 2 rewrite opp_involutive in H.
+intros n m H. apply opp_wd in H. now rewrite 2 opp_involutive in H.
 Qed.
 
 Theorem opp_inj_wd : forall n m, - n == - m <-> n == m.
@@ -135,7 +136,7 @@ Qed.
 Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.
 Proof.
 intros n m p; rewrite <- add_opp_r, opp_add_distr, add_assoc.
-now do 2 rewrite add_opp_r.
+now rewrite 2 add_opp_r.
 Qed.
 
 Theorem sub_sub_distr : forall n m p, n - (m - p) == (n - m) + p.
@@ -146,7 +147,7 @@ Qed.
 
 Theorem sub_opp_l : forall n m, - n - m == - m - n.
 Proof.
-intros n m. do 2 rewrite <- add_opp_r. now rewrite add_comm.
+intros n m. rewrite <- 2 add_opp_r. now rewrite add_comm.
 Qed.
 
 Theorem sub_opp_r : forall n m, n - (- m) == n + m.
@@ -163,7 +164,7 @@ Qed.
 Theorem sub_cancel_l : forall n m p, n - m == n - p <-> m == p.
 Proof.
 intros n m p. rewrite <- (add_cancel_l (n - m) (n - p) (- n)).
-do 2 rewrite add_sub_assoc. rewrite add_opp_diag_l; do 2 rewrite sub_0_l.
+rewrite 2 add_sub_assoc. rewrite add_opp_diag_l; rewrite 2 sub_0_l.
 apply opp_inj_wd.
 Qed.
 
@@ -250,6 +251,11 @@ Proof.
 intros; now rewrite <- sub_sub_distr, sub_diag, sub_0_r.
 Qed.
 
+Theorem sub_add : forall n m, m - n + n == m.
+Proof.
+ intros. now rewrite <- add_sub_swap, add_simpl_r.
+Qed.
+
 (** Now we have two sums or differences; the name includes the two
     operators and the position of the terms being canceled *)