proposition: Lemma diff_member_ly_rn a M N : a in M -> ~a in N -> a in (M - N).
proof: Proof. unfold member; intros H H0. rewrite diff_mult. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)