let n, k, i be Nat; :: thesis: (n div k) div i = n div (k * i)

now

per cases ( i = 0 or i <> 0 ) ;

suppose A1: i = 0 ; :: thesis: (n div k) div i = n div (k * i)

hence (n div k) div i = 0 by NAT_D:def 1
.= n div (k * i) by A1, NAT_D:def 1 ;
:: thesis: verum

end;

suppose A2: i <> 0 ; :: thesis: (n div k) div i = n div (k * i)

now

per cases ( k = 0 or k <> 0 ) ;

suppose A3: k = 0 ; :: thesis: (n div k) div i = n div (k * i)

then n div k = 0 by NAT_D:def 1;
hence (n div k) div i = n div (k * i) by A3, Th4; :: thesis: verum

end;

suppose A4: k <> 0 ; :: thesis: (n div k) div i = n div (k * i)

consider t2 being Nat such that
A5: n div k = (i * ((n div k) div i)) + t2 and
A6: t2 < i by A2, NAT_D:def 1;
t2 + 1 <= i by A6, NAT_1:13;
then A7: k * (t2 + 1) <= k * i by XREAL_1:66;
consider t1 being Nat such that
A8: n = (k * (n div k)) + t1 and
A9: t1 < k by A4, NAT_D:def 1;
(k * t2) + t1 < (k * t2) + (k * 1) by A9, XREAL_1:8;
then ((k * t2) + t1) - (k * i) < (k * (t2 + 1)) - (k * (t2 + 1)) by A7, XREAL_1:16;
then A10: (k * t2) + t1 < 0 + (k * i) by XREAL_1:21;
n = ((k * i) * ((n div k) div i)) + ((k * t2) + t1) by A8, A5;
hence (n div k) div i = n div (k * i) by A10, NAT_D:def 1; :: thesis: verum

end;

end;

end;

hence (n div k) div i = n div (k * i) ; :: thesis: verum

end;

end;

end;

hence (n div k) div i = n div (k * i) ; :: thesis: verum