theorem Th80: :: XREAL_1:80

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