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

6 files changed, 34 insertions, 0 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index 618722aa8..36f9c3d52 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -53,6 +53,11 @@ Proof.
 intros n m; now rewrite mul_opp_l, mul_opp_r, opp_involutive.
 Qed.
 
+Theorem mul_opp_comm : forall n m, (- n) * m == n * (- m).
+Proof.
+intros n m. now rewrite mul_opp_l, <- mul_opp_r.
+Qed.
+
 Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p.
 Proof.
 intros n m p. do 2 rewrite <- add_opp_r. rewrite mul_add_distr_l.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index c7795ab90..d0d64faa6 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -208,5 +208,9 @@ apply mul_lt_mono_nonneg.
 now apply lt_le_incl. assumption. apply le_0_1. assumption.
 Qed.
 
+(** Alternative name : *)
+
+Definition mul_eq_1 := eq_mul_1.
+
 End ZMulOrderProp.
 
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]]].
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index 804d1ccc0..1d6e8ba0a 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -74,5 +74,9 @@ assert (H3 : 1 < n * m) by now apply (lt_1_l m).
 rewrite H in H3; false_hyp H3 lt_irrefl.
 Qed.
 
+(** Alternative name : *)
+
+Definition mul_eq_1 := eq_mul_1.
+
 End NMulOrderProp.