let a, b be Real; :: thesis: ( b < 0 & a < - b implies - 1 < a / b )
assume that
A1: b < 0 and
A2: a < - b ; :: thesis: - 1 < a / b
assume a / b <= - 1 ; :: thesis: contradiction
then (a / b) * b >= (- 1) * b by A1, Lm28;
hence contradiction by A1, A2, XCMPLX_1:87; :: thesis: verum