let a, b be non zero Integer; :: thesis: ( Parity a > Parity b implies 2 * (Parity b) divides Parity a )
assume A1: Parity a > Parity b ; :: thesis: 2 * (Parity b) divides Parity a
A2: ( Parity a = 2 |^ (2 |-count a) & Parity b = 2 |^ (2 |-count b) ) by Def1;
then 2 |-count a > 2 |-count b by A1, PREPOWER:93;
then 2 |-count a >= (2 |-count b) + 1 by NAT_1:13;
then 2 |^ ((2 |-count b) + 1) divides 2 |^ (2 |-count a) by NEWTON:89;
hence 2 * (Parity b) divides Parity a by A2, NEWTON:6; :: thesis: verum