proposition: Lemma in_mult_S : forall (t : elt) (l : list elt), In t l -> multiplicity (list_to_multiset l) t >= 1.
proof: Proof. intro t; unfold list_to_multiset; induction l. contradiction. simpl; intro H; elim H; clear H. intro H; subst t; elim (eq_elt_dec a a). intros _ ; auto with arith. intro; absurd (a=a); trivial. elim (eq_elt_dec a t). intros _ _; auto with arith. intros; simpl; apply IHl; assumption. Qed.
imports: decidable_set List more_list Multiset Arith Setoid