lemma ListUtils.distinct_map, and several lemmas about list-oriented partitions:
* lemma remove_from_eq_class_preserves_disjoint
* lemma insert_into_member_list_distinct
* lemma partition_without_covers_list
* reordered some lemmas by dependency to improve reusability
a variant of distinct_map already exists in List.thy, so we are not going to do our own
Merge branch 'master' of https://github.com/formare/auctions