let i, j, k be Integer; :: thesis: ( j > 0 & k > 0 implies (i div j) div k = i div (j * k) )
assume A1: ( j > 0 & k > 0 ) ; :: thesis: (i div j) div k = i div (j * k)
set A = [\([\(i / j)/] / k)/];
set D = [\(i / (j * k))/];

A2: now

assume [\([\(i / j)/] / k)/] < [\(i / (j * k))/] ; :: thesis: contradiction
then A3: [\([\(i / j)/] / k)/] + 1 <= [\(i / (j * k))/] by INT_1:20;
(i / j) - 1 < [\(i / j)/] by INT_1:def 4;
then A4: i / j < [\(i / j)/] + 1 by XREAL_1:21;
[\(i / (j * k))/] <= i / (j * k) by INT_1:def 4;
then [\(i / (j * k))/] * k <= (i / (j * k)) * k by A1, XREAL_1:66;
then [\(i / (j * k))/] * k <= ((i / j) / k) * k by XCMPLX_1:79;
then A5: [\(i / (j * k))/] * k <= i / j by A1, XCMPLX_1:88;
([\(i / j)/] / k) - 1 < [\([\(i / j)/] / k)/] by INT_1:def 4;
then [\(i / j)/] / k < [\([\(i / j)/] / k)/] + 1 by XREAL_1:21;
then [\(i / j)/] / k < [\(i / (j * k))/] by A3, XXREAL_0:2;
then ([\(i / j)/] / k) * k < [\(i / (j * k))/] * k by A1, XREAL_1:70;
then [\(i / j)/] < [\(i / (j * k))/] * k by A1, XCMPLX_1:88;
then [\(i / j)/] + 1 <= [\(i / (j * k))/] * k by INT_1:20;
hence contradiction by A4, A5, XXREAL_0:2; :: thesis: verum

end;

A6: now

assume [\(i / (j * k))/] < [\([\(i / j)/] / k)/] ; :: thesis: contradiction
then A7: [\(i / (j * k))/] + 1 <= [\([\(i / j)/] / k)/] by INT_1:20;
(i / (j * k)) - 1 < [\(i / (j * k))/] by INT_1:def 4;
then A8: ( [\(i / j)/] <= i / j & [\([\(i / j)/] / k)/] <= [\(i / j)/] / k & i / (j * k) < [\(i / (j * k))/] + 1 ) by INT_1:def 4, XREAL_1:21;
then [\(i / j)/] / k <= (i / j) / k by A1, XREAL_1:74;
then [\(i / j)/] / k <= i / (j * k) by XCMPLX_1:79;
then [\([\(i / j)/] / k)/] <= i / (j * k) by A8, XXREAL_0:2;
hence contradiction by A7, A8, XXREAL_0:2; :: thesis: verum

end;

[\([\(i / j)/] / k)/] = [\(i / j)/] div k by INT_1:def 7;
then ( [\([\(i / j)/] / k)/] = (i div j) div k & [\(i / (j * k))/] = i div (j * k) ) by INT_1:def 7;
hence (i div j) div k = i div (j * k) by A2, A6, XXREAL_0:1; :: thesis: verum