let a, b be Real; :: thesis: ( a <= 0 & b < a implies a / b < 1 )
assume that
A1: a <= 0 and
A2: b < a ; :: thesis: a / b < 1
a / b < b / b by A1, A2, Lm29;
hence a / b < 1 by A1, A2, XCMPLX_1:60; :: thesis: verum