proposition: Lemma insert_remove_noteq a a' M : ~a =A= a' -> remove a (insert a' M) =mul= insert a' (remove a M).
proof: Proof. intros. apply multeq_meq. intro x; mset_unfold. repeat progress (try rewrite union_mult; try rewrite diff_mult). destruct (eqA_dec x a). rewrite !(singleton_mult_in e), (@singleton_mult_notin x a'). lia. rewrite e; auto with sets. rewrite (@singleton_mult_notin x a); trivial. destruct (eqA_dec x a'). solve_meq. solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)