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

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

suppose a >= 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, Lm10; :: thesis: verum

end;

suppose a < 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;

end;