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