Prove paper↔algorithm equivalence for the complete combinatorial Vickrey auction

[clange]

We so far have paper↔algorithm equivalence proofs for

• all partitions of a set (in Partitions.thy)
• all injective functions (in RelationProperties.thy)
• arg max (in Maximum.thy) – but needs revision (see Revise new “arg max” formalisation #18)

These three need to be combined (should be straightforward) into a paper↔algorithm equivalence proof of winning_allocation_rel vs. winning_allocation_alg_MC (or winning_allocation_alg_CL – which one, this depends on #18).

We also need such a proof for payments_rel vs. payments_alg, but here it's really straightforward, as on "paper" the payments are already defined as a function that almost looks computable.