theorem :: NEWTON05:75

for a being Nat holds
( Parity (a - (Parity a)) >= 2 * (Parity a) or a = Parity a )