for a, b being Integer st a < b holds
a <= b - 1