proposition: Lemma nb_occ_app : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) a (l1 l2 : list (A * B)), nb_occ eqA a (l1++l2) = nb_occ eqA a l1 + nb_occ eqA a l2.
proof: Proof. intros A B eqA a l1; induction l1 as [ | [a1 b1] l1]; simpl; trivial. intro l2; rewrite IHl1; destruct (eqA a a1) as [_ | _]; trivial. Qed.
imports: List Arith