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