theorem :: XREAL_1:72

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