proposition: Lemma multiplicity_in: forall l x, multiplicity (list_contents eqA_dec l) x > 0 -> exists x', eqA x' x /\ In x' l.
proof: Proof. induction l; simpl; intros. lia. destruct (eqA_dec a x). exists a; auto. destruct (IHl x) as [x' [x'x x'l]]; trivial. exists x'; split; auto. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)