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.