theorem :: NAT_2:30

for i, j, k being Nat holds (i -' j) -' k = i -' (j + k)