Library Coq.Numbers.Integer.Binary.ZBinary
Implementation of ZAxiomsSig by BinInt.Z
Bi-directional induction.
Basic operations.
Order
Properties specific to integers, not natural numbers.
Absolute value and sign
The instantiation of operations.
Placing them at the very end avoids having indirections in above lemmas.
Z forms a ring