let a be non zero Integer; :: thesis: a / (Parity a) = a div (Parity a)
( Parity a > 0 & Parity a divides a ) by Th3;
then A1: a mod (Parity a) = 0 by INT_1:62;
a / (Parity a) = (((a div (Parity a)) * (Parity a)) + (a mod (Parity a))) / (Parity a) by INT_1:59
.= ((a div (Parity a)) * (Parity a)) / (Parity a) by A1 ;
hence a / (Parity a) = a div (Parity a) by XCMPLX_1:89; :: thesis: verum