theorem :: XREAL_1:202

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