proposition: Lemma meq_remove a M N : insert a M =mul= N -> M =mul= remove a N.
proof: Proof. intros. rewrite <- H. solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)