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