let a, b be non zero Integer; :: thesis: ( Parity a divides Parity b iff Parity b >= Parity a )
A1: ( Parity a = 2 |^ (2 |-count a) & Parity b = 2 |^ (2 |-count b) ) by Def1;
( Parity b >= Parity a implies Parity a divides Parity b )

proof

assume Parity b >= Parity a ; :: thesis: Parity a divides Parity b
then 2 |-count b >= 2 |-count a by A1, PEPIN:66;
hence Parity a divides Parity b by A1, NEWTON:89; :: thesis: verum

end;

hence ( Parity a divides Parity b iff Parity b >= Parity a ) by NAT_D:7; :: thesis: verum