let a, b be real number ; :: thesis: ( a <= 0 & a <= b implies a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 ))) )
assume A1: ( a <= 0 & a <= b ) ; :: thesis: a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 )))

now

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 A1, Lm8; :: thesis: verum

end;

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

A3: b ^2 >= 0 by XREAL_1:65;
sqrt (1 + (b ^2 )) > 0 by A3, Th93;
then A4: a * (sqrt (1 + (b ^2 ))) <= 0 by A1;
A5: a ^2 >= 0 by XREAL_1:65;
sqrt (1 + (a ^2 )) > 0 by A5, Th93;
hence a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 ))) by A2, A4; :: thesis: verum

end;

end;

end;

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