for n being non zero Nat holds n - ((n div 2) * 2) <= 1