proposition: Lemma singleton_mult_notin : forall x y, ~x =A= y -> x / {{y}} = 0.
proof: Proof. intros; compute. case (eqA_dec x y); [contr | trivial]. Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)