let k, m, n be Nat; :: 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 12;

A4: now :: thesis: 1 <= x

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

end;

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