1 files changed, 87 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NMul.v b/theories/Numbers/Natural/Abstract/NMul.v
new file mode 100644
index 00000000..0b00f689
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NMul.v
@@ -0,0 +1,87 @@
+(************************************************************************)
+(*  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: NMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+
+Require Export NAdd.
+
+Module NMulPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NAddPropMod := NAddPropFunct NAxiomsMod.
+Open Local Scope NatScope.
+
+Theorem mul_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2.
+Proof NZmul_wd.
+
+Theorem mul_0_l : forall n : N, 0 * n == 0.
+Proof NZmul_0_l.
+
+Theorem mul_succ_l : forall n m : N, (S n) * m == n * m + m.
+Proof NZmul_succ_l.
+
+(** Theorems that are valid for both natural numbers and integers *)
+
+Theorem mul_0_r : forall n, n * 0 == 0.
+Proof NZmul_0_r.
+
+Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.
+Proof NZmul_succ_r.
+
+Theorem mul_comm : forall n m : N, n * m == m * n.
+Proof NZmul_comm.
+
+Theorem mul_add_distr_r : forall n m p : N, (n + m) * p == n * p + m * p.
+Proof NZmul_add_distr_r.
+
+Theorem mul_add_distr_l : forall n m p : N, n * (m + p) == n * m + n * p.
+Proof NZmul_add_distr_l.
+
+Theorem mul_assoc : forall n m p : N, n * (m * p) == (n * m) * p.
+Proof NZmul_assoc.
+
+Theorem mul_1_l : forall n : N, 1 * n == n.
+Proof NZmul_1_l.
+
+Theorem mul_1_r : forall n : N, n * 1 == n.
+Proof NZmul_1_r.
+
+(* Theorems that cannot be proved in NZMul *)
+
+(* In proving the correctness of the definition of multiplication on
+integers constructed from pairs of natural numbers, we'll need the
+following fact about natural numbers:
+
+a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u = a * m' + v
+
+Here n + m' == n' + m expresses equality of integers (n, m) and (n', m'),
+since a pair (a, b) of natural numbers represents the integer a - b. On
+integers, the formula above could be proved by moving a * m to the left,
+factoring out a and replacing n - m by n' - m'. However, the formula is
+required in the process of constructing integers, so it has to be proved
+for natural numbers, where terms cannot be moved from one side of an
+equation to the other. The proof uses the cancellation laws add_cancel_l
+and add_cancel_r. *)
+
+Theorem add_mul_repl_pair : forall a n m n' m' u v : N,
+  a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
+Proof.
+intros a n m n' m' u v H1 H2.
+apply (@NZmul_wd a a) in H2; [| reflexivity].
+do 2 rewrite mul_add_distr_l in H2. symmetry in H2.
+pose proof (NZadd_wd _ _ H1 _ _ H2) as H3.
+rewrite (add_shuffle1 (a * m)), (add_comm (a * m) (a * n)) in H3.
+do 2 rewrite <- add_assoc in H3. apply -> add_cancel_l in H3.
+rewrite (add_assoc u), (add_comm (a * m)) in H3.
+apply -> add_cancel_r in H3.
+now rewrite (add_comm (a * n') u), (add_comm (a * m') v).
+Qed.
+
+End NMulPropFunct.
+