proposition: Theorem number_of_occurrences_O : forall a l, ~ In a l -> number_of_occurrences a l = 0.
proof: Proof. intros a l; elim l; simpl in |- *; auto. intros a0 l0 H H0; case (A_eq_dec a a0); auto. intros H1; case H0; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)