for x being non zero Nat holds 0 in x