proposition: Lemma multiplicity_In : forall l a, In a l <-> 0 < multiplicity (list_contents l) a.
proof: Proof. intros; split; intro H. - eapply In_InA, multiplicity_InA in H; eauto with typeclass_instances. - eapply multiplicity_InA, InA_alt in H as (y & -> & H); eauto with typeclass_instances. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation