for k being non zero Nat holds (k -' 1) + 2 = (k + 2) -' 1