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