let
i
,
j
,
k
be
Nat
;
:: thesis:
(
j
+
k
<=
i
implies
k
<=
i
-'
j
)
assume
A1
:
j
+
k
<=
i
;
:: thesis:
k
<=
i
-'
j
per
cases
(
j
+
k
=
i
or
j
+
k
<
i
)
by
A1
,
XXREAL_0:1
;
suppose
j
+
k
=
i
;
:: thesis:
k
<=
i
-'
j
hence
k
<=
i
-'
j
by
NAT_D:34
;
:: thesis:
verum
end;
suppose
j
+
k
<
i
;
:: thesis:
k
<=
i
-'
j
hence
k
<=
i
-'
j
by
Lm2
;
:: thesis:
verum
end;
end;