theorem :: NAT_D:38

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