theorem :: NEWTON05:91

for a being odd Nat holds
( Parity (a + 1) = 2 iff parity (a div 2) = 0 )