for a, b being Nat holds
( ( parity (a + b) = parity b implies parity a = 0 ) & ( parity (a + b) <> parity b implies parity a = 1 ) )