MODULE Inequality;

PRED NotZero(x) IS 
  (E y ~ x :: x * y = 1) 
END;

PRED NotEqual(x, y) IS 
  NotZero(x - y) 
END;

PRED NonNeg(x) IS 
  (E y ~ 1 :: y * y = x) 
END;

PRED NonPos(x) IS NonNeg(-x) END;

PRED Pos(x) IS 
  NonNeg(x) AND NotZero(x) 
END;

PRED Neg(x) IS Pos(-x) END;

PRED Greater(x, y) IS Pos(x - y) END;

PRED Less(x, y) IS Pos(y - x) END;

PRED AtLeast(x, y) IS 
  NonNeg(x - y) 
END;

PRED AtMost(x, y) IS AtLeast(y, x) END;

PRED LeftOf(a, b) IS 
  AtMost(CAR(a), CAR(b)) 
END;

UI PointTool(LeftOf);