Library Coq.Numbers.Natural.Abstract.NMul



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.

Theorem mul_0_l : forall n : N, 0 * n == 0.

Theorem mul_succ_l : forall n m : N, (S n) * m == n * m + m.

Theorems that are valid for both natural numbers and integers

Theorem mul_0_r : forall n, n * 0 == 0.

Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.

Theorem mul_comm : forall n m : N, n * m == m * n.

Theorem mul_add_distr_r : forall n m p : N, (n + m) * p == n * p + m * p.

Theorem mul_add_distr_l : forall n m p : N, n * (m + p) == n * m + n * p.

Theorem mul_assoc : forall n m p : N, n * (m * p) == (n * m) * p.

Theorem mul_1_l : forall n : N, 1 * n == n.

Theorem mul_1_r : forall n : N, n * 1 == n.



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.



End NMulPropFunct.