let a be Integer; :: thesis: for b being non zero Integer st not b divides a holds
(a div b) + ((- a) div b) = - 1
let b be non zero Integer; :: thesis: ( not b divides a implies (a div b) + ((- a) div b) = - 1 )
assume A1: not b divides a ; :: thesis: (a div b) + ((- a) div b) = - 1
reconsider a = a as non zero Integer by A1, INT_2:12;
A2: ( a div b = [\(a / b)/] & (- a) div b = [\((- a) / b)/] ) by INT_1:def 9;
(a / b) * b = a by XCMPLX_1:87;
then a / b is not Integer by A1;
then - [\(a / b)/] = [\((- a) / b)/] + 1 by INT_1:63;
then [\(a / b)/] + [\((- a) / b)/] = - 1 ;
hence (a div b) + ((- a) div b) = - 1 by A2; :: thesis: verum