theorem :: NEWTON05:80

for a, b being non zero Integer holds
( Parity a > Parity b iff ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even ) )