theorem :: XREAL_1:204
for a, b being Real st b < 0 & - a <= b holds
a / b <= - 1