let i, k, n be Nat; ( k divides n & 1 <= n & 1 <= i & i <= k implies (n -' i) div k = (n div k) - 1 )
assume that
A1:
k divides n
and
A2:
1 <= n
and
A3:
1 <= i
and
A4:
i <= k
; (n -' i) div k = (n div k) - 1
A5:
k -' i < k
by A3, A4, Th9;
A6:
k <= n
by A1, A2, NAT_D:7;
then
i + k <= k + n
by A4, XREAL_1:7;
then A7:
i <= n
by XREAL_1:6;
n div k > 0
then
n div k >= 0 + 1
by NAT_1:13;
then A8:
(n div k) -' 1 = (n div k) - 1
by XREAL_1:233;
n = k * (n div k)
by A1, NAT_D:3;
then n -' i =
(((k * (n div k)) - (k * 1)) + k) - i
by A7, XREAL_1:233
.=
(k * ((n div k) -' 1)) + (k - i)
by A8
.=
(k * ((n div k) -' 1)) + (k -' i)
by A4, XREAL_1:233
;
hence
(n -' i) div k = (n div k) - 1
by A8, A5, NAT_D:def 1; verum