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)))

- a <= - b by A2, XREAL_1:24;

then (- a) * (sqrt (1 + ((- b) ^2))) <= (- b) * (sqrt (1 + ((- a) ^2))) by A1, Lm2;

then - (a * (sqrt (1 + (b ^2)))) <= - (b * (sqrt (1 + (a ^2)))) ;

hence a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) by XREAL_1:24; :: thesis: verum

assume that

A1: a >= 0 and

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

- a <= - b by A2, XREAL_1:24;

then (- a) * (sqrt (1 + ((- b) ^2))) <= (- b) * (sqrt (1 + ((- a) ^2))) by A1, Lm2;

then - (a * (sqrt (1 + (b ^2)))) <= - (b * (sqrt (1 + (a ^2)))) ;

hence a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) by XREAL_1:24; :: thesis: verum