theorem :: NAT_D:53

for k, i, j being natural Number st i <= j + k holds
i -' k <= j