theorem :: XREAL_1:116
for a, b, c, d being Real st b < 0 & 0 < d & c / d < a * b holds
a * d < c / b