proposition: Theorem frequency_list_in : forall a n m, In (a, n) (frequency_list m) -> In a m.
proof: Proof. intros a n m; generalize n; elim m; clear m n; simpl in |- *; auto. intros a0 l H n H0; case add_frequency_list_in_inv with (1 := H0); auto. intros H1; right; apply (H n); auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)