theorem :: XREAL_1:102

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