let a, b be Integer; :: thesis: ( Parity a divides Parity b or Parity b divides Parity a )

per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose ( a = 0 or b = 0 ) ; :: thesis: ( Parity a divides Parity b or Parity b divides Parity a )

then ( Parity a = 0 or Parity b = 0 ) by Def1;
hence ( Parity a divides Parity b or Parity b divides Parity a ) by INT_2:12; :: thesis: verum

end;

suppose B1: ( a <> 0 & b <> 0 ) ; :: thesis: ( Parity a divides Parity b or Parity b divides Parity a )

then reconsider a = a as non zero Integer ;
reconsider b = b as non zero Integer by B1;
B2: ( Parity a = 2 |^ (2 |-count a) & Parity b = 2 |^ (2 |-count b) ) by Def1;

per cases ( 2 |-count a >= 2 |-count b or 2 |-count b >= 2 |-count a ) ;

suppose 2 |-count a >= 2 |-count b ; :: thesis: ( Parity a divides Parity b or Parity b divides Parity a )

hence ( Parity a divides Parity b or Parity b divides Parity a ) by B2, NEWTON:89; :: thesis: verum

end;

suppose 2 |-count b >= 2 |-count a ; :: thesis: ( Parity a divides Parity b or Parity b divides Parity a )

hence ( Parity a divides Parity b or Parity b divides Parity a ) by B2, NEWTON:89; :: thesis: verum

end;

end;

end;

end;