let k, x1, x2, y1, y2 be Nat; :: thesis: ( x2 <= k & x1 <= (k -' x2) + y2 implies ( x2 + (x1 -' y2) <= k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) ) )
assume Z0: x2 <= k ; :: thesis: ( not x1 <= (k -' x2) + y2 or ( x2 + (x1 -' y2) <= k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) ) )
then A1: k -' x2 = k - x2 by XREAL_1:233;
assume Z1: x1 <= (k -' x2) + y2 ; :: thesis: ( x2 + (x1 -' y2) <= k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) )
thus x2 + (x1 -' y2) <= k :: thesis: (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)

proof

per cases ( x1 < y2 or x1 >= y2 ) ;

suppose x1 < y2 ; :: thesis: x2 + (x1 -' y2) <= k

then x1 -' y2 = 0 by NAT_2:8;
hence x2 + (x1 -' y2) <= k by Z0; :: thesis: verum

end;

suppose x1 >= y2 ; :: thesis: x2 + (x1 -' y2) <= k

then x1 -' y2 = x1 - y2 by XREAL_1:233;
then ( x1 -' y2 <= ((k - x2) + y2) - y2 & ((k - x2) + y2) - y2 = k - x2 ) by A1, Z1, XREAL_1:9;
then x2 + (x1 -' y2) <= (k - x2) + x2 by XREAL_1:6;
hence x2 + (x1 -' y2) <= k ; :: thesis: verum

end;

end;

end;

then A2: ( k -' (x2 + (x1 -' y2)) = k - (x2 + (x1 -' y2)) & ((k -' x2) + y2) -' x1 = ((k - x2) + y2) - x1 ) by Z1, A1, XREAL_1:233;

per cases ( x1 <= y2 or x1 > y2 ) ;

suppose x1 <= y2 ; :: thesis: (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)

then ( x1 -' y2 = 0 & y2 -' x1 = y2 - x1 ) by XREAL_1:233, NAT_2:8;
hence (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) by A2; :: thesis: verum

end;

suppose x1 > y2 ; :: thesis: (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)

then ( y2 -' x1 = 0 & x1 -' y2 = x1 - y2 ) by XREAL_1:233, NAT_2:8;
hence (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) by A2; :: thesis: verum

end;

end;