let n be Nat; :: thesis: ( n is even implies n div 2 = (n + 1) div 2 )
assume A1: n is even ; :: thesis: n div 2 = (n + 1) div 2
n = (2 * (n div 2)) + (n mod 2) by NAT_D:2
.= (2 * (n div 2)) + 0 by A1, Th21 ;
hence n div 2 = (n + 1) div 2 by NAT_D:def 1; :: thesis: verum