proposition: Lemma multiplicity_of_app : forall l l' a, multiplicity a (l :: l') = (multiplicity a l + multiplicity a l')%nat.
proof: Proof. induction l; simpl; auto with arith. intros. case (T1_eq_dec a l1). rewrite IHl2. clear IHl1 IHl2; intro; omega. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0