let n be Nat; :: thesis: n -' 0 = n
n -' 0 = n - 0 by XREAL_0:def 2
.= n ;
hence n -' 0 = n ; :: thesis: verum