let i, j, k be Integer; :: thesis: ( k > 0 implies (i div j) div k = i div (j * k) )
set A = [\([\(i / j)/] / k)/];
set D = [\(i / (j * k))/];
[\([\(i / j)/] / k)/] = [\(i / j)/] div k by INT_1:def 9;
then A1: [\([\(i / j)/] / k)/] = (i div j) div k by INT_1:def 9;
assume A2: k > 0 ; :: thesis: (i div j) div k = i div (j * k)

A3: now :: thesis: not [\([\(i / j)/] / k)/] < [\(i / (j * k))/]

([\(i / j)/] / k) - 1 < [\([\(i / j)/] / k)/] by INT_1:def 6;
then A4: [\(i / j)/] / k < [\([\(i / j)/] / k)/] + 1 by XREAL_1:19;
assume [\([\(i / j)/] / k)/] < [\(i / (j * k))/] ; :: thesis: contradiction
then [\([\(i / j)/] / k)/] + 1 <= [\(i / (j * k))/] by INT_1:7;
then [\(i / j)/] / k < [\(i / (j * k))/] by A4, XXREAL_0:2;
then ([\(i / j)/] / k) * k < [\(i / (j * k))/] * k by A2, XREAL_1:68;
then [\(i / j)/] < [\(i / (j * k))/] * k by A2, XCMPLX_1:87;
then A5: [\(i / j)/] + 1 <= [\(i / (j * k))/] * k by INT_1:7;
[\(i / (j * k))/] <= i / (j * k) by INT_1:def 6;
then [\(i / (j * k))/] * k <= (i / (j * k)) * k by A2, XREAL_1:64;
then [\(i / (j * k))/] * k <= ((i / j) / k) * k by XCMPLX_1:78;
then A6: [\(i / (j * k))/] * k <= i / j by A2, XCMPLX_1:87;
(i / j) - 1 < [\(i / j)/] by INT_1:def 6;
then i / j < [\(i / j)/] + 1 by XREAL_1:19;
hence contradiction by A6, A5, XXREAL_0:2; :: thesis: verum

end;

A7: now :: thesis: not [\(i / (j * k))/] < [\([\(i / j)/] / k)/]

[\(i / j)/] <= i / j by INT_1:def 6;
then [\(i / j)/] / k <= (i / j) / k by A2, XREAL_1:72;
then ( [\([\(i / j)/] / k)/] <= [\(i / j)/] / k & [\(i / j)/] / k <= i / (j * k) ) by INT_1:def 6, XCMPLX_1:78;
then A8: [\([\(i / j)/] / k)/] <= i / (j * k) by XXREAL_0:2;
(i / (j * k)) - 1 < [\(i / (j * k))/] by INT_1:def 6;
then A9: i / (j * k) < [\(i / (j * k))/] + 1 by XREAL_1:19;
assume [\(i / (j * k))/] < [\([\(i / j)/] / k)/] ; :: thesis: contradiction
then [\(i / (j * k))/] + 1 <= [\([\(i / j)/] / k)/] by INT_1:7;
hence contradiction by A9, A8, XXREAL_0:2; :: thesis: verum

end;

[\(i / (j * k))/] = i div (j * k) by INT_1:def 9;
hence (i div j) div k = i div (j * k) by A3, A7, A1, XXREAL_0:1; :: thesis: verum