theorem OPC: :: NEWTON05:87

for a, b being non zero Integer holds
( Parity a, Oddity b are_coprime & (Parity a) gcd (Oddity b) = 1 )