theorem :: XREAL_1:75
for a, b, c being Real st c < 0 & a < b holds
b / c < a / c by Lm29;