theorem :: NAT_D:59

for k, n being natural Number st n < k holds
(k -' (n + 1)) + 1 = k -' n