( not
d
is
zero
iff
d
>=
1
+
0
)
by
NAT_1:13
;
hence
(
d
is
zero
iff not
d
>=
1 ) ;
:: thesis:
verum