let k be Integer; :: thesis: for n being Nat st n > 0 & k mod n <> 0 holds
- (k div n) = ((- k) div n) + 1
let n be Nat; :: thesis: ( n > 0 & k mod n <> 0 implies - (k div n) = ((- k) div n) + 1 )
assume A1: n > 0 ; :: thesis: ( not k mod n <> 0 or - (k div n) = ((- k) div n) + 1 )
assume k mod n <> 0 ; :: thesis: - (k div n) = ((- k) div n) + 1
then not n divides k by A1, INT_1:62;
then A2: k / n is not Integer by A1, Th17;
thus - (k div n) = - [\(k / n)/] by INT_1:def 9
.= [\((- k) / n)/] + 1 by A2, INT_1:63
.= ((- k) div n) + 1 by INT_1:def 9 ; :: thesis: verum