theorem :: NAT_2:27

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