1 files changed, 115 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
new file mode 100644
index 00000000..c48d1b4c
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -0,0 +1,115 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i $Id: ZMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+
+Require Export ZAdd.
+
+Module ZMulPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module Export ZAddPropMod := ZAddPropFunct ZAxiomsMod.
+Open Local Scope IntScope.
+
+Theorem Zmul_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2.
+Proof NZmul_wd.
+
+Theorem Zmul_0_l : forall n : Z, 0 * n == 0.
+Proof NZmul_0_l.
+
+Theorem Zmul_succ_l : forall n m : Z, (S n) * m == n * m + m.
+Proof NZmul_succ_l.
+
+(* Theorems that are valid for both natural numbers and integers *)
+
+Theorem Zmul_0_r : forall n : Z, n * 0 == 0.
+Proof NZmul_0_r.
+
+Theorem Zmul_succ_r : forall n m : Z, n * (S m) == n * m + n.
+Proof NZmul_succ_r.
+
+Theorem Zmul_comm : forall n m : Z, n * m == m * n.
+Proof NZmul_comm.
+
+Theorem Zmul_add_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p.
+Proof NZmul_add_distr_r.
+
+Theorem Zmul_add_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p.
+Proof NZmul_add_distr_l.
+
+(* A note on naming: right (correspondingly, left) distributivity happens
+when the sum is multiplied by a number on the right (left), not when the
+sum itself is the right (left) factor in the product (see planetmath.org
+and mathworld.wolfram.com). In the old library BinInt, distributivity over
+subtraction was named correctly, but distributivity over addition was named
+incorrectly. The names in Isabelle/HOL library are also incorrect. *)
+
+Theorem Zmul_assoc : forall n m p : Z, n * (m * p) == (n * m) * p.
+Proof NZmul_assoc.
+
+Theorem Zmul_1_l : forall n : Z, 1 * n == n.
+Proof NZmul_1_l.
+
+Theorem Zmul_1_r : forall n : Z, n * 1 == n.
+Proof NZmul_1_r.
+
+(* The following two theorems are true in an ordered ring,
+but since they don't mention order, we'll put them here *)
+
+Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
+Proof NZeq_mul_0.
+
+Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZneq_mul_0.
+
+(* Theorems that are either not valid on N or have different proofs on N and Z *)
+
+Theorem Zmul_pred_r : forall n m : Z, n * (P m) == n * m - n.
+Proof.
+intros n m.
+rewrite <- (Zsucc_pred m) at 2.
+now rewrite Zmul_succ_r, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
+Qed.
+
+Theorem Zmul_pred_l : forall n m : Z, (P n) * m == n * m - m.
+Proof.
+intros n m; rewrite (Zmul_comm (P n) m), (Zmul_comm n m). apply Zmul_pred_r.
+Qed.
+
+Theorem Zmul_opp_l : forall n m : Z, (- n) * m == - (n * m).
+Proof.
+intros n m. apply -> Zadd_move_0_r.
+now rewrite <- Zmul_add_distr_r, Zadd_opp_diag_l, Zmul_0_l.
+Qed.
+
+Theorem Zmul_opp_r : forall n m : Z, n * (- m) == - (n * m).
+Proof.
+intros n m; rewrite (Zmul_comm n (- m)), (Zmul_comm n m); apply Zmul_opp_l.
+Qed.
+
+Theorem Zmul_opp_opp : forall n m : Z, (- n) * (- m) == n * m.
+Proof.
+intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive.
+Qed.
+
+Theorem Zmul_sub_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p.
+Proof.
+intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite Zmul_add_distr_l.
+now rewrite Zmul_opp_r.
+Qed.
+
+Theorem Zmul_sub_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p.
+Proof.
+intros n m p; rewrite (Zmul_comm (n - m) p), (Zmul_comm n p), (Zmul_comm m p);
+now apply Zmul_sub_distr_l.
+Qed.
+
+End ZMulPropFunct.
+
+