proposition: Theorem number_of_occurrences_app : forall l1 l2 a, number_of_occurrences a (l1 ++ l2) = number_of_occurrences a l1 + number_of_occurrences a l2.
proof: Proof. intros l1; elim l1; simpl in |- *; auto. intros a l H l2 a0; case (A_eq_dec a0 a); intros H1; simpl in |- *; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)