take 2 * ((2 * 0) + 1) ; :: thesis: 2 * ((2 * 0) + 1) is double_odd
thus 2 * ((2 * 0) + 1) is double_odd ; :: thesis: verum