theorem :: NAT_6:5

for n being natural odd number holds n div 2 = (n - 1) / 2