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

suppose a = 0 ; :: thesis: Parity a is square

hence Parity a is square by Def1; :: thesis: verum

end;

suppose a <> 0 ; :: thesis: Parity a is square

then reconsider a = a as non zero Integer ;
Parity a = 2 |^ (dwa |-count a) by Def1;
hence Parity a is square ; :: thesis: verum

end;

end;