Library Coq.Numbers.Integer.Abstract.ZMul
A note on naming: right (correspondingly, left) distributivity
happens when the sum is multiplied by a number on the right
(left), not when the sum itself is the right (left) factor in the
product (see planetmath.org and mathworld.wolfram.com). In the old
library BinInt, distributivity over subtraction was named
correctly, but distributivity over addition was named
incorrectly. The names in Isabelle/HOL library are also
incorrect.
Theorems that are either not valid on N or have different proofs
on N and Z
Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
Theorem mul_pred_l : forall n m, (P n) * m == n * m - m.
Theorem mul_opp_l : forall n m, (- n) * m == - (n * m).
Theorem mul_opp_r : forall n m, n * (- m) == - (n * m).
Theorem mul_opp_opp : forall n m, (- n) * (- m) == n * m.
Theorem mul_opp_comm : forall n m, (- n) * m == n * (- m).
Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p.
Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
End ZMulProp.