new lemma Max_Im_ge_lower_bound
more progress in wd_outcome non-negative payments case that participant n gets everything