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