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

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

suppose a = 0 ; :: thesis: a / b <= 1

hence a / b <= 1 ; :: thesis: verum

end;

suppose A3: a < 0 ; :: thesis: a / b <= 1

then a / b <= b / b by A1, Lm30;
hence a / b <= 1 by A1, A3, XCMPLX_1:60; :: thesis: verum

end;

end;