theorem :: NAT_D:55

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