# Library Coq.Numbers.Integer.Abstract.ZMul

Module ZMulPropFunct (Import ZAxiomsMod : ZAxiomsSig).
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.