Proof of mset_mem_iff_count_nzero