let
n
be non
zero
Nat
;
:: thesis:
(
n

1 is
Nat
& 1
<=
n
)
A1
:
0
+
1
<=
n
by
NAT_1:13
;
then
(
0
+
1)

1
<=
n

1
by
XREAL_1:9
;
then
n

1
in
NAT
by
INT_1:3
;
hence
n

1 is
Nat
;
:: thesis:
1
<=
n
thus
1
<=
n
by
A1
;
:: thesis:
verum