theorem :: PRE_FF:5

for i, j, k being Integer st k >= 0 holds
(i div j) div k = i div (j * k)