theorem :: XREAL_1:201

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