proposition: Lemma member_list_multiset : forall l, forall x, In x l -> member x (list2multiset l).
proof: Proof. induction l. intros x x_In_nil; absurd (In x nil); auto. simpl; intros x x_In_al; case x_In_al. intro ax; rewrite ax; apply member_insert. intro x_In_l; mset_unfold. rewrite union_mult. assert ((x/(list2multiset l))%msets > 0). apply (IHl x); trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)