proposition: Lemma in_mul_sum : forall xs X Y x, list2multiset xs =mul= X + Y -> x in X -> exists x', x =A= x' /\ In x' xs.
proof: Proof. intros. assert (x_xs: x in (list2multiset xs)). rewrite H. apply member_member_union; trivial. destruct (member_multiset_list xs x_xs). exists x0; auto. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)