proposition: Lemma member_member_union a M N : a in M -> a in (M+N).
proof: Proof. unfold member; intros. replace (a/(M+N)) with ((a/M)%msets + (a/N)%msets)%nat. lia. auto with multisets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)