proposition: Lemma mem_memrem M a b : ~ a =A= b -> a in M -> a in (M - {{b}}).
proof: Proof. compute; intros. rewrite diff_mult. rewrite singleton_mult_notin. lia. trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)