for n, n1, n2 being Nat st n1 + n <= n2 + 1 & n > 0 holds
n1 <= n2