for k, n being Nat holds
( k - n in Seg k iff n < k )