theorem :: NEWTON05:81

for a being odd Nat holds Parity (a - 1) = 2 * (Parity (a div 2))