theorem :: XREAL_1:118

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