let le x y = Z.cmp x y <= 0