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;