renamed parent → partition_without and cleaned up lemmas about it
using set comprehension syntax for partition_without (but this requires a new lemma image_Collect_mem)
renamed l13 → partition_without_covers, simplified proof
renamed l3 → partition_without_is_partition, simplified proof
renamed partitionsconstructor → all_coarser_partitions_with
restored some subsequent proofs, which the previous commit had broken
(with two exceptions into which I'll look later)