proposition: Theorem frequency_number_of_occurrences : forall a m, In a m -> In (a, number_of_occurrences a m) (frequency_list m).
proof: Proof. intros a m; generalize a; elim m; clear m a; simpl in |- *; auto. intros a l H a0 H0; case (A_eq_dec a0 a); simpl in |- *; auto. intros e; case (In_dec A_eq_dec a0 l). intros H1; rewrite e; apply add_frequency_list_in; auto. apply (H a); rewrite <- e; auto. intros H1; rewrite number_of_occurrences_O; auto. rewrite e; apply add_frequency_list_1. intros ca; contradict H1; auto. rewrite e; apply frequency_list_in with (1 := H1). intros H1; case H0; auto. intros H2; case H1; auto. intros H3; apply add_frequency_list_not_in; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)