Submit Partitions.thy, RelationProperties.thy and their dependencies to the AFP

[clange]

Submission guidelines

probably best as separate entries:

1. Partitions
2. RelationProperties (mainly: injective functions)
3. Common dependencies

[caminati]

As a byproduct of further auction theory theorems in d.thy, now there is much more stuff in c.thy regarding relations. For example:

1. quotientation by equivalence relations.
2. kernel of a function as a partition of its domain.
3. compatibility (when does quotientation preserve runiq?).
4. passing from a partition to its equivalence relation (e.g., in case 2 we get the equivalence relation of all the preimages of the same elements).