theorem Th77: :: XREAL_1:77
for a, b, c being Real st 0 < b & a * b <= c holds
a <= c / b