let a, b be non zero Integer; :: thesis: ( Parity a > Parity b iff ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even ) )
thus ( Parity a > Parity b implies ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even ) ) :: thesis: ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even implies Parity a > Parity b )

proof

assume Parity a > Parity b ; :: thesis: ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even )
then 2 * (Parity b) divides Parity a by P2P;
then consider c being Integer such that
A1: Parity a = (2 * (Parity b)) * c ;
(0 + ((2 * c) * (Parity b))) div (Parity b) = (0 div (Parity b)) + (2 * c) by NAT_D:61;
hence ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even ) by A1; :: thesis: verum

end;

assume ( not (Parity a) div (Parity b) is zero & (Parity a) div (Parity b) is even ) ; :: thesis: Parity a > Parity b
then B1: (Parity b) * ((Parity a) div (Parity b)) >= 2 * (Parity b) by NAT_D:7, NEWTON02:2;
B2: 2 * (Parity b) > 1 * (Parity b) by XREAL_1:68;
((Parity b) * ((Parity a) div (Parity b))) + ((Parity a) mod (Parity b)) >= ((Parity b) * ((Parity a) div (Parity b))) + 0 by XREAL_1:6;
then Parity a >= ((Parity b) * ((Parity a) div (Parity b))) + 0 by INT_1:59;
then Parity a >= 2 * (Parity b) by B1, XXREAL_0:2;
hence Parity a > Parity b by B2, XXREAL_0:2; :: thesis: verum