Allow for partial allocations of goods

[clange]

We already have a partial variant of RelationProperties.injections. We would additionally need a partial variant of injections_alg. This would have to be realised by recursing not just on the tail xs, but on all sublists x # xs of length n - 1. Reuse some library code (List.{sublist,sublists,n_lists}).

In CombinatorialAuction.thy we would have to provide variants of possible_allocations_*.