started lemma remaining_value_rel for payment well-definedness
renamed confusing "buyer" to "x" (i.e. some allocation)