for n, k being Nat st n < k holds
n <= k - 1