let n, m, k be Nat; :: thesis: (n + k) -' (m + k) = n -' m
A1: (n + k) - (m + k) = n - m ;

per cases ( n - m >= 0 or n - m < 0 ) ;

suppose n - m >= 0 ; :: thesis: (n + k) -' (m + k) = n -' m

then n -' m = n - m by XREAL_0:def 2;
hence (n + k) -' (m + k) = n -' m by A1, XREAL_0:def 2; :: thesis: verum

end;

suppose A2: n - m < 0 ; :: thesis: (n + k) -' (m + k) = n -' m

then n -' m = 0 by XREAL_0:def 2;
hence (n + k) -' (m + k) = n -' m by A1, A2, XREAL_0:def 2; :: thesis: verum

end;

end;