theorem Th1: :: PRGCOR_1:1

for n, m, k being Nat holds (n + k) -' (m + k) = n -' m