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