Library Coq.ZArith.Zmax
Maximum of two binary integer numbers
Definition Zmax m n :=
match m ?=
n with
|
Eq |
Gt =>
m
|
Lt =>
n
end.
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