theorem :: XREAL_1:103

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