let
a
,
b
,
r
be
Real
;
:: thesis:
(
r
>=
0
&
a
+
r
<=
b
implies
a
<=
b
)
assume
(
r
>=
0
&
a
+
r
<=
b
) ;
:: thesis:
a
<=
b
then
(
(
a
+
r
)

r
<=
b

r
&
b

r
<=
b
)
by
XREAL_1:9
,
XREAL_1:43
;
hence
a
<=
b
by
XXREAL_0:2
;
:: thesis:
verum