finish proof of total_pad_len_Zlist, fix proof of lemma 2, not sure how to deal with <> (one-to-one). contrapositive?