theorem :: XREAL_1:189

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