let a, b be non zero Integer; :: thesis: ( Parity a > Parity b implies a div (Parity b) is even )
assume Parity a > Parity b ; :: thesis: a div (Parity b) is even
then A0: 2 * (Parity b) divides Parity a by P2P;
Parity a divides a by Th3;
then 2 * (Parity b) divides a by INT_2:9, A0;
then consider c being Integer such that
A1: a = (2 * (Parity b)) * c ;
(0 + ((2 * c) * (Parity b))) div (Parity b) = (0 div (Parity b)) + (2 * c) by NAT_D:61;
hence a div (Parity b) is even by A1; :: thesis: verum