let
k
,
n
be
Nat
;
:: thesis:
n

k
<=
n
n
<=
n
+
k
by
NAT_1:11
;
hence
n

k
<=
n
by
XREAL_1:20
;
:: thesis:
verum