let a be even Integer; :: thesis: a div 2 = (a + 1) div 2
(((a + 1) div 2) * 2) + ((a + 1) mod 2) = a + 1 by INT_1:59
.= (((a div 2) * 2) + (a mod 2)) + 1 by INT_1:59
.= ((a div 2) * 2) + ((a + 1) mod 2) ;
hence a div 2 = (a + 1) div 2 ; :: thesis: verum