Some migration of results from BinInt to Numbers

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

3 files changed, 21 insertions, 0 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 202875b8a..8bed3027f 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -30,6 +30,11 @@ intros n m; nzinduct n. now nzsimpl.
 intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
+Theorem add_succ_comm : forall n m, S n + m == n + S m.
+Proof.
+intros n m. now rewrite add_succ_r, add_succ_l.
+Qed.
+
 Hint Rewrite add_0_r add_succ_r : nz.
 
 Theorem add_comm : forall n m, n + m == m + n.
@@ -82,6 +87,11 @@ Proof.
 intros n m p q. rewrite (add_comm p). apply add_shuffle1.
 Qed.
 
+Theorem add_shuffle3 : forall n m p, n + (m + p) == m + (n + p).
+Proof.
+intros n m p. now rewrite add_comm, <- add_assoc, (add_comm p).
+Qed.
+
 Theorem sub_1_r : forall n, n - 1 == P n.
 Proof.
 intro n; now nzsimpl'.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 33c50b24e..2b5a1cf33 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -81,4 +81,9 @@ Proof.
 intros n m p q. rewrite (mul_comm p). apply mul_shuffle1.
 Qed.
 
+Theorem mul_shuffle3 : forall n m p, n * (m * p) == m * (n * p).
+Proof.
+intros n m p. now rewrite mul_assoc, (mul_comm n), mul_assoc.
+Qed.
+
 End NZMulProp.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 7061dddcd..30a475aea 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -241,6 +241,12 @@ intros n m H1 H2; apply eq_mul_0 in H1. destruct H1 as [H1 | H1].
 false_hyp H1 H2. assumption.
 Qed.
 
+(** Some alternative names: *)
+
+Definition mul_eq_0 := eq_mul_0.
+Definition mul_eq_0_l := eq_mul_0_l.
+Definition mul_eq_0_r := eq_mul_0_r.
+
 Theorem lt_0_mul : forall n m, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
 Proof.
 intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].