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