Library Coq.ZArith.Znat
Binary Integers (Pierre Crégut, CNET, Lannion, France)
Properties of the injection from nat into Z
Injection and successor
Injection and equality.
Injection and order relations:
One way ...
The other way ...
Injection and usual operations
Composition of injections
Misc