proposition: Lemma multiplicity_app : forall (l1 l2:list elt) (t : elt), multiplicity (list_to_multiset (l1 ++ l2)) t = multiplicity (list_to_multiset l1) t + multiplicity (list_to_multiset l2) t.
proof: Proof. induction l1; intros; trivial. simpl; intros; rewrite (IHl1 l2 t); auto with arith. Qed.
imports: decidable_set List more_list Multiset Arith Setoid