Library Coq.ZArith.Zmax
THIS FILE IS DEPRECATED. Use Zminmax instead.
Zmax is now Zminmax.Zmax. Code that do things like
unfold Zmin.Zmin will have to be adapted, and neither
a Definition or a Notation here can help much.
Characterization of maximum on binary integer numbers
Least upper bound properties of max
Semi-lattice properties of max
Additional properties of max
Operations preserving max
Characterization of Pminus in term of Zminus and Zmax