let
k
be
Element
of
NAT
;
:: thesis:
( not
k
is
zero
iff 1
<=
k
)
hereby
:: thesis:
( 1
<=
k
implies not
k
is
zero
)
assume
not
k
is
zero
;
:: thesis:
1
<=
k
then
0
+
1
<=
k
by
NAT_1:13
;
hence
1
<=
k
;
:: thesis:
verum
end;
assume
1
<=
k
;
:: thesis:
not
k
is
zero
hence
not
k
is
zero
;
:: thesis:
verum