let a, b be real number ; :: thesis: ( a < 0 & b <= a implies 1 <= b / a )
assume that
A1: a < 0 and
A2: b <= a ; :: thesis: 1 <= b / a
b / a >= a / a by A1, A2, Lm30;
hence 1 <= b / a by A1, XCMPLX_1:60; :: thesis: verum