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

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

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

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

end;

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

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

end;

end;