let b, a be real number ; :: thesis: ( b < 0 & - a <= b implies a / b <= - 1 )
assume A1: b < 0 ; :: thesis: ( not - a <= b or a / b <= - 1 )
assume A2: - a <= b ; :: thesis: a / b <= - 1
assume a / b > - 1 ; :: thesis: contradiction
then (a / b) * b < (- 1) * b by A1, Lm24;
then a < - b by A1, XCMPLX_1:87;
hence contradiction by A2, Th28; :: thesis: verum