Description: Extend class notation with the upper integer function. Read " ZZ>=M " as "the set of integers greater than or equal to M ".