Proof of nat_plus_inc_int_nzero