theorem :: XREAL_1:113

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