proposition: Lemma multiplicity_In_S : forall l a, In a l -> multiplicity (list_contents l) a >= 1.
proof: Proof. intros l a; rewrite multiplicity_In; auto. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation