let i, k, n be Nat; :: thesis: ( 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 ; :: thesis: (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

proof

assume not n div k > 0 ; :: thesis: contradiction
then n div k = 0 ;
hence contradiction by A3, A4, A6, Th12; :: thesis: verum

end;

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; :: thesis: verum