take 0 ; :: thesis: 0 is even
0 = 2 * 0 ;
hence 0 is even ; :: thesis: verum