let m, n, x, y be Nat; :: thesis: ( n = (m -' x) + y implies ( m -' n <= x & n -' m <= y ) )
assume A0: n = (m -' x) + y ; :: thesis: ( m -' n <= x & n -' m <= y )

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

suppose m <= n ; :: thesis: ( m -' n <= x & n -' m <= y )

then A1: ( m -' n = 0 & n -' m = n - m ) by NAT_2:8, XREAL_1:233;
n <= m + y by A0, XREAL_1:6, NAT_D:35;
hence ( m -' n <= x & n -' m <= y ) by A1, XREAL_1:20; :: thesis: verum

end;

suppose m > n ; :: thesis: ( m -' n <= x & n -' m <= y )

then A2: ( n -' m = 0 & m -' (m -' n) = n & n >= m -' x ) by A0, NAT_D:58, NAT_1:11, NAT_2:8;
( m -' (m -' n) = m - (m -' n) & m -' x >= m - x ) by XREAL_0:def 2, XREAL_1:233, NAT_D:35;
then m - (m -' n) >= m - x by A2, XXREAL_0:2;
hence ( m -' n <= x & n -' m <= y ) by XREAL_1:10, A2; :: thesis: verum

end;

end;