proposition: Lemma list2multiset_mult : forall l a, a / (list2multiset l) = multiplicity (list_contents eqA_dec l) a.
proof: Proof. induction l; intros. auto with multisets. simpl; unfold insert. rewrite union_mult. destruct (eqA_dec a a0). rewrite singleton_mult_in; auto with sets. rewrite singleton_mult_notin; auto with sets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)