theorem :: FINSEQ_3:13

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