let a, b be real number ; :: 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

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

end;

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

b ^2 >= 0 by XREAL_1:65;
then sqrt (1 + (b ^2 )) > 0 by Th93;
then A4: a * (sqrt (1 + (b ^2 ))) <= 0 by A1;
a ^2 >= 0 by XREAL_1:65;
then sqrt (1 + (a ^2 )) > 0 by Th93;
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