proposition: Lemma list2multiset_remove_in a : forall m, remove a (list2multiset m) =mul= list2multiset (removeElem eqA eqA_dec a m).
proof: Proof. induction m; simpl; intros. solve_meq. destruct (eqA_dec a a0); simpl. rewrite <- (insert_remove_eq (list2multiset m) e); auto with multisets. rewrite (insert_remove_noteq (list2multiset m) n). rewrite IHm; auto with multisets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)