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

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

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

hence a / b <= 1 ; :: thesis: verum

end;

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

then a / b <= b / b by A1, Lm25;
hence a / b <= 1 by A1, A3, XCMPLX_1:60; :: thesis: verum

end;

end;