take 1 ; :: thesis: not 1 is even
1 = (2 * 0) + 1 ;
hence not 1 is even ; :: thesis: verum