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