for i, j being non zero Nat holds i -' j < i