theorem FOT1: :: MOEBIUS2:3

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