proposition: Theorem compute_pbcode_not_null : forall p, compute_pbcode p <> [].
proof: Proof. intros p; elim p; simpl in |- *; auto; try (intros p0; case (compute_pbcode p0); simpl in |- *; auto); intros; red in |- *; intros HH1; discriminate. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)