Proof of mset_count_bound_for_union