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