theorem :: XREAL_1:104

for a, b, c, d being Real st 0 < b & d < 0 & a * d <= c * b holds
c / d <= a / b