proposition: Lemma mult_comp : forall l a, a / l = multiplicity (list_contents eqA eqA_dec l) a.
proof: Proof. induction l. auto. intro a0; simpl. destruct (eqA_dec a0 a); destruct (eqA_dec a a0); simpl; rewrite <- (IHl a0); (reflexivity || absurd (a0 =A= a); auto with sets). Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)