let x, y be Real; :: thesis: ( y > 0 implies (min (x,y)) / (max (x,y)) <= 1 )
assume A1: y > 0 ; :: thesis: (min (x,y)) / (max (x,y)) <= 1

per cases ( x > 0 or x <= 0 ) ;

suppose A2: x > 0 ; :: thesis: (min (x,y)) / (max (x,y)) <= 1

now :: thesis: (min (x,y)) / (max (x,y)) <= 1

per cases ( x >= y or x < y ) ;

suppose A3: x >= y ; :: thesis: (min (x,y)) / (max (x,y)) <= 1

then ( max (x,y) = x & min (x,y) = y ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence (min (x,y)) / (max (x,y)) <= 1 by A1, A3, XREAL_1:183; :: thesis: verum

end;

suppose A4: x < y ; :: thesis: (min (x,y)) / (max (x,y)) <= 1

then ( max (x,y) = y & min (x,y) = x ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence (min (x,y)) / (max (x,y)) <= 1 by A2, A4, XREAL_1:183; :: thesis: verum

end;

end;

end;

hence (min (x,y)) / (max (x,y)) <= 1 ; :: thesis: verum

end;

suppose A5: x <= 0 ; :: thesis: (min (x,y)) / (max (x,y)) <= 1

then ( min (x,y) = x & max (x,y) = y ) by A1, XXREAL_0:def 9, XXREAL_0:def 10;
hence (min (x,y)) / (max (x,y)) <= 1 by A1, A5; :: thesis: verum

end;

end;