factored out stuff from proofs of lemma CombinatorialVickreyAuctionSoundness.remaining_value_alt and lemma CombinatorialVickreyAuctionSoundness.wd_outcome to make it reusable:
* CombinatorialAuctionProperties.allocs_finite
* CombinatorialVickreyAuctionSoundness.card_goods_gt_0
* CombinatorialVickreyAuctionSoundness.finite_goods
* CombinatorialVickreyAuctionSoundness.card_participants_gt_0
* CombinatorialVickreyAuctionSoundness.finite_participants
* CombinatorialVickreyAuctionSoundness.finite_participants_except
* fun winning_allocation_except
* lemma winning_allocation_except_subrel