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