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