let k be Integer; :: thesis: for n being Nat st k mod n = 0 holds
- (k div n) = (- k) div n
let n be Nat; :: thesis: ( k mod n = 0 implies - (k div n) = (- k) div n )
assume A1: k mod n = 0 ; :: thesis: - (k div n) = (- k) div n

per cases ( n > 0 or n = 0 ) ;

suppose A2: n > 0 ; :: thesis: - (k div n) = (- k) div n

then n divides k by A1, INT_1:62;
then A3: k / n is Integer by A2, Th17;
thus - (k div n) = - [\(k / n)/] by INT_1:def 9
.= [\((- k) / n)/] by A3, INT_1:64
.= (- k) div n by INT_1:def 9 ; :: thesis: verum

end;

suppose n = 0 ; :: thesis: - (k div n) = (- k) div n

hence - (k div n) = (- k) div n ; :: thesis: verum

end;

end;