for n being Nat
for z being non zero Nat holds
not for k being Nat holds not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1)