proposition: Lemma meq_ins_rem a M : a in M -> M =mul= M - {{a}} + {{a}}.
proof: Proof. mset_unfold; intros. apply multeq_meq; intro. rewrite union_mult. rewrite diff_mult. case (eqA_dec x a); intro x_a. rewrite singleton_mult_in; trivial. assert (x/M = a/M). apply mult_eqA_compat; trivial. lia. rewrite !singleton_mult_notin. lia. trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)