proposition: Lemma insert_remove_eq a a' M : a =A= a' -> M =mul= remove a (insert a' M).
proof: Proof. intros. apply multeq_meq. intro x; mset_unfold. rewrite diff_mult. rewrite union_mult. destruct (eqA_dec x a). rewrite !singleton_mult_in; eauto with sets. lia. rewrite !singleton_mult_notin; eauto with sets. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)