reconsider e = - 1 as Integer ;
e * n is even ;
hence - n is even ; :: thesis: verum