let a, b be Real; :: thesis: ( a <= 0 & a <= b implies a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )
assume that
A1: a <= 0 and
A2: a <= b ; :: thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

now :: thesis: ( ( b <= 0 & a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) ) or ( b > 0 & a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) ) )

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

case b <= 0 ; :: thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

hence a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by A2, Lm1; :: thesis: verum

end;

case A3: b > 0 ; :: thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

b ^2 >= 0 by XREAL_1:63;
then sqrt (1 + (b ^2)) > 0 by SQUARE_1:25;
then A4: a * (sqrt (1 + (b ^2))) <= 0 by A1;
a ^2 >= 0 by XREAL_1:63;
then sqrt (1 + (a ^2)) > 0 by SQUARE_1:25;
hence a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by A3, A4; :: thesis: verum

end;

end;

end;

hence a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) ; :: thesis: verum