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

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

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

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

end;

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

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

end;

end;