let a, b be Real; :: thesis: ( 0 <= b & - 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, Lm13;
hence contradiction by A2, A3, XCMPLX_1:87; :: thesis: verum

end;

end;