for n, m, k being Nat st m <= k & n < m holds
k -' m < k -' n