Library Coq.Numbers.Integer.Abstract.ZAdd
Theorems that are either not valid on N or have different proofs
on N and Z
The next several theorems are devoted to moving terms from one
side of an equation to the other. The name contains the operation
in the original equation (add or sub) and the indication
whether the left or right term is moved.
The two theorems above do not allow rewriting subformulas of the
form n - m == p to n == p + m since subtraction is in the
right-hand side of the equation. Hence the following two
theorems.
The following section is devoted to cancellation of like
terms. The name includes the first operator and the position of
the term being canceled.
Now we have two sums or differences; the name includes the two
operators and the position of the terms being canceled
Of course, there are many other variants