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

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

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

then A1: ( m -' n = 0 & n -' m = n - m ) by NAT_2:8, XREAL_1:233;
then m -' (m -' n) = m by NAT_D:40;
hence n = (m -' (m -' n)) + (n -' m) by A1; :: thesis: verum

end;

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

then ( n -' m = 0 & m -' (m -' n) = n & n + 0 = n ) by NAT_D:58, NAT_2:8;
hence n = (m -' (m -' n)) + (n -' m) ; :: thesis: verum

end;

end;