let a, b, c, d be Real; :: thesis: ( 0 < b & d < 0 & a * d <= c * b implies c / d <= a / b )
assume that
A1: b > 0 and
A2: d < 0 and
A3: a * d <= c * b ; :: thesis: c / d <= a / b
(a * d) / b <= c by A1, A3, Th79;
then (a / b) * d <= c by XCMPLX_1:74;
hence c / d <= a / b by A2, Th78; :: thesis: verum