theorem :: XREAL_1:182

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