proposition: Theorem number_of_occurrences_permutation : forall l1 l2 a, Permutation l1 l2 -> number_of_occurrences a l1 = number_of_occurrences a l2.
proof: Proof. intros l1 l2 a H; generalize a; elim H; clear H a l1 l2; simpl in |- *; auto. intros a L1 L2 H H0 a0; case (A_eq_dec a a0); simpl in |- *; auto; case (A_eq_dec a0 a); simpl in |- *; auto. intros a b L a0; case (A_eq_dec a0 a); simpl in |- *; auto; case (A_eq_dec a0 b); simpl in |- *; auto. intros L1 L2 L3 H H0 H1 H2 a; apply trans_equal with (1 := H0 a); auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)