let k be Integer; for n being natural number st n > 0 & k mod n <> 0 holds
- (k div n) = ((- k) div n) + 1
let n be natural number ; ( n > 0 & k mod n <> 0 implies - (k div n) = ((- k) div n) + 1 )
assume A1:
n > 0
; ( not k mod n <> 0 or - (k div n) = ((- k) div n) + 1 )
assume
k mod n <> 0
; - (k div n) = ((- k) div n) + 1
then
not n divides k
by A1, INT_1:89;
then A2:
k / n is not Integer
by A1, Th22;
thus - (k div n) =
- [\(k / n)/]
by INT_1:def 7
.=
[\((- k) / n)/] + 1
by A2, INT_1:90
.=
((- k) div n) + 1
by INT_1:def 7
; verum