proposition: Theorem not_null_m : m <> [].
proof: Proof. Proof using frequency_more_than_one. generalize frequency_more_than_one; case m; simpl in |- *; auto. intros H; contradict H; auto with arith. intros; discriminate. Qed.
imports: Coq(Sorting.Permutation) Huffman(Code BTree Build PBTree2BTree Restrict)