theorem :: XREAL_1:120

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