let k be Integer; :: thesis: for n being natural number st n > 0 & k mod n = 0 holds
- (k div n) = (- k) div n
let n be natural number ; :: thesis: ( n > 0 & k mod n = 0 implies - (k div n) = (- k) div n )
assume A1: n > 0 ; :: thesis: ( not k mod n = 0 or - (k div n) = (- k) div n )
assume k mod n = 0 ; :: thesis: - (k div n) = (- k) div n
then n divides k by A1, INT_1:62;
then A2: k / n is Integer by A1, Th22;
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