proposition: Lemma multiplicity_InA_O : forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
proof: Proof. intros l a; rewrite multiplicity_InA; destruct (multiplicity (list_contents l) a); auto with arith. destruct 1; auto with arith. Qed.
imports: Lia Relations Multiset SetoidList