proposition: Lemma out_mult_O : forall (t : elt) (l:list elt), ~ In t l -> multiplicity (list_to_multiset l) t = 0.
proof: Proof. intro t; unfold list_to_multiset; induction l. intros _; trivial. intro H; simpl; elim (eq_elt_dec a t). intro; subst t; absurd (In a (a :: l)); trivial; left; trivial. intros _; apply IHl; unfold not; intros; apply H; simpl; right; assumption. Qed.
imports: decidable_set List more_list Multiset Arith Setoid