let a, b be Real; :: thesis: ( 0 < b & b <= - a implies a / b <= - 1 )
assume A1: b > 0 ; :: thesis: ( not b <= - a or a / b <= - 1 )
assume A2: b <= - a ; :: thesis: a / b <= - 1
assume a / b > - 1 ; :: thesis: contradiction
then (a / b) * b > (- 1) * b by A1, Lm13;
then a > - b by A1, XCMPLX_1:87;
hence contradiction by A2, Th25; :: thesis: verum