let
i
,
j
be
Nat
;
:: thesis:
( not
i
<=
j
or
i
=
j
or
i
+
1
<=
j
)
assume
i
<=
j
;
:: thesis:
(
i
=
j
or
i
+
1
<=
j
)
then
i
+
1
<=
j
+
1
by
XREAL_1:6
;
hence
(
i
=
j
or
i
+
1
<=
j
)
by
NAT_1:8
,
XCMPLX_1:2
;
:: thesis:
verum