Library Coq.Numbers.Integer.Abstract.ZMul
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.
Theorem Zmul_0_l :
forall n :
Z, 0 *
n == 0.
Theorem Zmul_succ_l :
forall n m :
Z, (
S n) *
m ==
n *
m +
m.
Theorem Zmul_0_r :
forall n :
Z,
n * 0 == 0.
Theorem Zmul_succ_r :
forall n m :
Z,
n * (
S m) ==
n *
m +
n.
Theorem Zmul_comm :
forall n m :
Z,
n *
m ==
m *
n.
Theorem Zmul_add_distr_r :
forall n m p :
Z, (
n +
m) *
p ==
n *
p +
m *
p.
Theorem Zmul_add_distr_l :
forall n m p :
Z,
n * (
m +
p) ==
n *
m +
n *
p.
Theorem Zmul_assoc :
forall n m p :
Z,
n * (
m *
p) == (
n *
m) *
p.
Theorem Zmul_1_l :
forall n :
Z, 1 *
n ==
n.
Theorem Zmul_1_r :
forall n :
Z,
n * 1 ==
n.
Theorem Zeq_mul_0 :
forall n m :
Z,
n *
m == 0 <->
n == 0 \/
m == 0.
Theorem Zneq_mul_0 :
forall n m :
Z,
n ~= 0 /\
m ~= 0 <->
n *
m ~= 0.
Theorem Zmul_pred_r :
forall n m :
Z,
n * (
P m) ==
n *
m -
n.
Theorem Zmul_pred_l :
forall n m :
Z, (
P n) *
m ==
n *
m -
m.
Theorem Zmul_opp_l :
forall n m :
Z, (-
n) *
m == - (
n *
m).
Theorem Zmul_opp_r :
forall n m :
Z,
n * (-
m) == - (
n *
m).
Theorem Zmul_opp_opp :
forall n m :
Z, (-
n) * (-
m) ==
n *
m.
Theorem Zmul_sub_distr_l :
forall n m p :
Z,
n * (
m -
p) ==
n *
m -
n *
p.
Theorem Zmul_sub_distr_r :
forall n m p :
Z, (
n -
m) *
p ==
n *
p -
m *
p.
End ZMulPropFunct.