let n, m be Nat; :: thesis: m -' n >= m - n
thus m -' n >= m - n by XREAL_0:def 2; :: thesis: verum