let b, d, a, c be real number ; :: thesis: ( b < 0 & 0 < d & 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, Th82;
then (a / b) * d >= c by XCMPLX_1:75;
hence c / d <= a / b by A2, Th81; :: thesis: verum