let i, j be Nat; :: thesis: ( i <= j implies i + (j -' i) = (i + j) -' i )
assume i <= j ; :: thesis: i + (j -' i) = (i + j) -' i
then 0 <= j - i by XREAL_1:48;
then A1: j -' i = j - i by XREAL_0:def 2;
(i + j) -' i = (i + j) - i by XREAL_0:def 2;
hence i + (j -' i) = (i + j) -' i by A1; :: thesis: verum