((- 1) / 3) - 1 < - 1 ;
then [\((- 1) / 3)/] = - 1 by INT_1:def 6;
hence (- 1) div 3 = - 1 by INT_1:def 9; :: thesis: verum