theorem :: NAT_6:5

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