let c, b, a be real number ; :: thesis: ( 0 <= c & b <= a implies b / c <= a / c )
assume A1: ( 0 <= c & 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 c " = 0 ;
then ( b * (c " ) = 0 & a * (c " ) = 0 ) ;
then ( b / c = 0 & a / c = 0 ) by XCMPLX_0:def 9;
hence b / c <= a / c ; :: thesis: verum

end;

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

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

end;

end;