let i, j, k, l be Nat; ( k <> 0 & i < l & l <= j & k divides l implies i div k < j div k )
assume that
A1:
k <> 0
and
A2:
i < l
and
A3:
l <= j
and
A4:
k divides l
; i div k < j div k
A5:
l mod k = 0
by A1, A4, PEPIN:6;
i + (i mod k) >= i
by NAT_1:11;
then
i - (i mod k) <= (i + (i mod k)) - (i mod k)
by XREAL_1:9;
then
i - (i mod k) < l
by A2, XXREAL_0:2;
then A6:
(i - (i mod k)) / k < l / k
by A1, XREAL_1:74;
i = (k * (i div k)) + (i mod k)
by A1, NAT_D:2;
then
(k / k) * (i div k) = (i - (i mod k)) / k
;
then A7:
1 * (i div k) = (i - (i mod k)) / k
by A1, XCMPLX_1:60;
l =
(k * (l div k)) + (l mod k)
by A1, NAT_D:2
.=
k * (l div k)
by A5
;
then
(k / k) * (l div k) = l / k
;
then A8:
1 * (l div k) = l / k
by A1, XCMPLX_1:60;
l div k <= j div k
by A3, NAT_2:24;
hence
i div k < j div k
by A8, A7, A6, XXREAL_0:2; verum