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

per cases ( j + k = i or j + k < i ) by A1, XXREAL_0:1;

suppose j + k = i ; :: thesis: k <= i -' j

hence k <= i -' j by NAT_D:34; :: thesis: verum

end;

suppose j + k < i ; :: thesis: k <= i -' j

hence k <= i -' j by Lm2; :: thesis: verum

end;

end;