theorem Th11: :: PRGCOR_1:11

for n, m being Integer
for n2, m2 being Element of NAT holds
( ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) & ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) )