proposition: Lemma member_meq_union a M N M' N' : M + N =mul= M' + N' -> (a in M \/ a in N) -> ~a in N' -> a in M'.
proof: Proof. mset_unfold; intros. assert (((a/M)%msets + (a/N)%msets)%nat = ((a/M')%msets + (a/N')%msets)%nat). rewrite <- !union_mult. apply meq_multeq; trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)