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