let a, b be Real; :: 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, Lm9; :: 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, Lm7; :: thesis: verum

end;

end;