theorem :: NAT_2:26

for n being Nat st n is even holds
n div 2 = (n + 1) div 2