for n, m being Nat holds m -' n >= m - n by XREAL_0:def 2;