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