theorem :: XREAL_1:73

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