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

suppose p >= 0 ; :: thesis: not p |^ n is square

then p in NAT by INT_1:3;
hence not p |^ n is square ; :: thesis: verum

end;

suppose p < 0 ; :: thesis: not p |^ n is square

hence not p |^ n is square ; :: thesis: verum

end;

end;