for i, k, n being Nat holds (n div k) div i = n div (k * i)