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

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

hence Oddity a is square ; :: thesis: verum

end;

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

then reconsider a = a as non zero Integer ;
a = (Parity a) * (Oddity a) ;
hence Oddity a is square ; :: thesis: verum

end;

end;