for n, k being Nat st k in Segm (n + 1) holds
n - k is Nat