factored out lemma winning_allocation_injective for reuse in lemma remaining_value_alt and lemma wd_outcome