theorem :: XREAL_1:185

for a, b being Real st 0 <= a & b <= a holds
b / a <= 1 by Lm38;