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 A0: k mod n = 0 ; :: thesis: - (k div n) = (- k) div n

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

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

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

end;

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

( k div 0 = 0 & (- k) div 0 = 0 ) by INT_1:48;
hence - (k div n) = (- k) div n by A3; :: thesis: verum

end;

end;