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