let a, b be Real; :: thesis: ( b <= 0 & b <= - a implies - 1 <= a / b )
assume b <= 0 ; :: thesis: ( not b <= - a or - 1 <= a / b )

per cases then ( b = 0 or b < 0 ) ;

suppose b = 0 ; :: thesis: ( not b <= - a or - 1 <= a / b )

then b " = 0 ;
then a * (b ") = 0 ;
hence ( not b <= - a or - 1 <= a / b ) by XCMPLX_0:def 9; :: thesis: verum

end;

suppose A2: b < 0 ; :: thesis: ( not b <= - a or - 1 <= a / b )

assume A3: b <= - a ; :: thesis: - 1 <= a / b
assume a / b < - 1 ; :: thesis: contradiction
then (a / b) * b > (- 1) * b by A2, Lm24;
then a > - b by A2, XCMPLX_1:87;
hence contradiction by A3, Th25; :: thesis: verum

end;

end;