let a, b be Integer; :: thesis: a div b = (- a) div (- b)
a div b = [\(a / b)/] by INT_1:def 9
.= [\((- a) / (- b))/] by XCMPLX_1:191
.= (- a) div (- b) by INT_1:def 9 ;
hence a div b = (- a) div (- b) ; :: thesis: verum