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