let n, m, k be Nat; :: thesis: ( m <= k & n < m implies k -' m < k -' n )
assume that
A1: m <= k and
A2: n < m ; :: thesis: k -' m < k -' n
A3: k - m < k - n by A2, XREAL_1:15;
k -' n = k - n by A1, A2, XREAL_1:233, XXREAL_0:2;
hence k -' m < k -' n by A1, A3, XREAL_1:233; :: thesis: verum