reconsider b = a / 2 as Integer ;
((2 * b) + 1) mod 2 = 1 mod 2 by NAT_D:61;
hence (a + 1) mod 2 = 1 by NAT_D:14; :: thesis: verum