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;