theorem :: XREAL_1:196

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