Library Coq.ZArith.Zminmax
Maximum and Minimum of two Z numbers
Local Open Scope Z_scope.
The functions Zmax and Zmin implement indeed
a maximum and a minimum
We obtain hence all the generic properties of max and min.
Properties specific to the Z domain
Compatibilities (consequences of monotonicity)
Anti-monotonicity swaps the role of min and max
Compatibility with Zpos
Characterization of Pminus in term of Zminus and Zmax