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

suppose a >= 0 ; :: thesis: not a |^ n is negative

hence not a |^ n is negative ; :: thesis: verum

end;

suppose a < 0 ; :: thesis: not a |^ n is negative

hence not a |^ n is negative ; :: thesis: verum

end;

end;