for i being Integer holds i div 1 = i