take 0 ; :: thesis: not 0 is negative
thus not 0 is negative ; :: thesis: verum