let i, j, k be Nat; :: thesis: ( i -' k <= j implies i <= j + k )
assume A1: i -' k <= j ; :: thesis: i <= j + k

per cases ( i >= k or i <= k ) ;

suppose A2: i >= k ; :: thesis: i <= j + k

(i -' k) + k <= j + k by A1, XREAL_1:6;
hence i <= j + k by A2, XREAL_1:235; :: thesis: verum

end;

suppose A3: i <= k ; :: thesis: i <= j + k

k <= j + k by NAT_1:11;
hence i <= j + k by A3, XXREAL_0:2; :: thesis: verum

end;

end;