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