proposition: Lemma member_union_l a M N : a in M -> a in (M + N).
proof: Proof. unfold member; intro H. rewrite union_mult. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)