theorem Th78: :: XREAL_1:78

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