let k, n, m be natural number ; :: thesis: ( k in Seg n & m < k implies k - m in Seg n )
assume that
A1: k in Seg n and
A2: m < k ; :: thesis: k - m in Seg n
consider i being Nat such that
A3: k = m + i by A2, NAT_1:10;
reconsider x = k - m as Element of NAT by A3, ORDINAL1:def 13;

A4: now

assume not 1 <= x ; :: thesis: contradiction
then x = 0 by NAT_1:14;
hence contradiction by A2; :: thesis: verum

end;

( i <= k & k <= n ) by A1, A3, FINSEQ_1:3, NAT_1:12;
then x <= n by A3, XXREAL_0:2;
hence k - m in Seg n by A4, FINSEQ_1:3; :: thesis: verum