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