theorem Th79: :: XREAL_1:79

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