theorem :: XREAL_1:115

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