proposition: Lemma meq_insert_remove a M : a in M -> insert a (remove a M) =mul= M.
proof: Proof. intros. apply multeq_meq; intro x. unfold insert, remove. rewrite union_mult. rewrite diff_mult. destruct (eqA_dec x a). rewrite singleton_mult_in; trivial. rewrite (mult_eqA_compat M e). unfold member in H. lia. rewrite singleton_mult_notin; trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)