let a, b be Real; :: thesis: ( b <= a & 0 <= a implies b / a <= 1 )
assume A1: b <= a ; :: thesis: ( not 0 <= a or b / a <= 1 )
assume A2: a >= 0 ; :: thesis: b / a <= 1

per cases ( a = 0 or a > 0 ) by A2;

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

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

end;

suppose A3: a > 0 ; :: thesis: b / a <= 1

assume b / a > 1 ; :: thesis: contradiction
then (b / a) * a > 1 * a by A3, Lm13;
hence contradiction by A1, A3, XCMPLX_1:87; :: thesis: verum

end;

end;