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

7 files changed, 37 insertions, 31 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index 618722aa81..36f9c3d527 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 c7795ab90b..d0d64faa60 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 202875b8ac..8bed3027f6 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 33c50b24eb..2b5a1cf338 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 7061dddcdd..30a475aeab 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 804d1ccc0c..1d6e8ba0a3 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.
 
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index eaf30e6d0e..d07fe5174b 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1295,17 +1295,7 @@ Proof.
  rewrite geb_leb. apply leb_spec.
 Qed.
 
-(** TODO : to add in Numbers *)
-
-Lemma add_shuffle3 n m p : n + (m + p) = m + (n + p).
-Proof.
- now rewrite add_comm, <- add_assoc, (add_comm p).
-Qed.
-
-Lemma mul_shuffle3 n m p : n * (m * p) = m * (n * p).
-Proof.
- now rewrite mul_assoc, (mul_comm n), mul_assoc.
-Qed.
+(** TODO : to add in Numbers ? *)
 
 Lemma add_reg_l n m p : n + m = n + p -> m = p.
 Proof.
@@ -1322,25 +1312,6 @@ Proof.
  exact (fun Hp => proj1 (mul_cancel_r n m p Hp)).
 Qed.
 
-Lemma add_succ_comm n m : succ n + m = n + succ m.
-Proof.
- now rewrite add_succ_r, add_succ_l.
-Qed.
-
-Lemma mul_opp_comm n m : - n * m = n * - m.
-Proof.
- now destruct n, m.
-Qed.
-
-Notation mul_eq_0 := eq_mul_0.
-
-Lemma mul_eq_0_l n m : n <> 0 -> m * n = 0 -> m = 0.
-Proof.
- intros Hn H. apply eq_mul_0 in H. now destruct H.
-Qed.
-
-Notation mul_eq_1 := eq_mul_1.
-
 Lemma opp_eq_mul_m1 n : - n = n * -1.
 Proof.
  rewrite mul_comm. now destruct n.
@@ -1466,7 +1437,6 @@ Notation Zmult_1_r := Z.mul_1_r (only parsing).
 Notation Zmult_comm := Z.mul_comm (only parsing).
 Notation Zmult_assoc := Z.mul_assoc (only parsing).
 Notation Zmult_permute := Z.mul_shuffle3 (only parsing).
-Notation Zmult_integral_l := Z.mul_eq_0_l (only parsing).
 Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing).
 Notation Zdouble_mult := Z.double_spec (only parsing).
 Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing).
@@ -1550,6 +1520,8 @@ Lemma Zmult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
 Proof (SYM3 Z.mul_assoc).
 Lemma Zmult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.
 Proof (fun n m => proj1 (Z.mul_eq_0 n m)).
+Lemma Zmult_integral_l : forall n m, n <> 0 -> m * n = 0 -> m = 0.
+Proof (fun n m H H' => Z.mul_eq_0_l m n H' H).
 Lemma Zopp_mult_distr_l : forall n m, - (n * m) = - n * m.
 Proof (SYM2 Z.mul_opp_l).
 Lemma Zopp_mult_distr_r : forall n m, - (n * m) = n * - m.