let a, c, b be real number ; :: thesis: ( 0 < a & 0 <= c & a <= b implies c / b <= c / a )
assume that
A1: 0 < a and
A2: 0 <= c and
A3: a <= b ; :: thesis: c / b <= c / a
A4: 0 <= b " by A1, A3;
A5: 0 <= a " by A1;
a * (b " ) <= b * (b " ) by A3, A4, Lm12;
then a * (b " ) <= 1 by A1, A3, XCMPLX_0:def 7;
then (a " ) * (a * (b " )) <= (a " ) * 1 by A5, Lm12;
then ((a " ) * a) * (b " ) <= a " ;
then 1 * (b " ) <= a " by A1, XCMPLX_0:def 7;
then c * (b " ) <= c * (a " ) by A2, Lm12;
then c / b <= c * (a " ) by XCMPLX_0:def 9;
hence c / b <= c / a by XCMPLX_0:def 9; :: thesis: verum