let
n
,
m
,
k
be
Nat
;
:: thesis:
(
k
<
m
implies
n
+
k
in
n
+
m
)
assume
m
>
k
;
:: thesis:
n
+
k
in
n
+
m
then
k
+
n
<
n
+
m
by
XREAL_1:8
;
then
n
+
k
in
Segm
(
n
+
m
)
by
NAT_1:44
;
hence
n
+
k
in
n
+
m
;
:: thesis:
verum