let a, b, c be Real; :: thesis: ( 0 <= c & b <= a implies b / c <= a / c )
assume that
A1: 0 <= c and
A2: b <= a ; :: thesis: b / c <= a / c

per cases ( c = 0 or 0 < c ) by A1;

suppose c = 0 ; :: thesis: b / c <= a / c

then A3: c " = 0 ;
then b * (c ") = 0 ;
then A4: b / c = 0 by XCMPLX_0:def 9;
a * (c ") = 0 by A3;
hence b / c <= a / c by A4, XCMPLX_0:def 9; :: thesis: verum

end;

suppose A5: 0 < c ; :: thesis: b / c <= a / c

assume a / c < b / c ; :: thesis: contradiction
then (a / c) * c < (b / c) * c by A5, Lm13;
then a < (b / c) * c by A5, XCMPLX_1:87;
hence contradiction by A2, A5, XCMPLX_1:87; :: thesis: verum

end;

end;