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.