let a, b, c be Real; :: thesis: ( b < 0 & a * b < c implies c / b < a )
assume that
A1: b < 0 and
A2: a * b < c ; :: thesis: c / b < a
(a * b) / b > c / b by A1, A2, Lm29;
hence c / b < a by A1, XCMPLX_1:89; :: thesis: verum