new lemma ex_allocations (factored out from CombinatorialVickreyAuctionSoundness.wd_outcome)
more in first step of "payments non-negative" part of wd_outcome