theorem :: NEWTON05:42

for a being Nat holds Parity (2 * a) = 2 * (Parity a)