theorem :: PRE_FF:2

for i being Integer holds i div 1 = i