theorem :: NAT_6:4

for n being even Nat holds n div 2 = n / 2