for i, j being Nat st j < i holds
(i -' (j + 1)) + 1 = i -' j