for i being Integer holds i mod i = 0