proposition: Theorem pbbuild_true_pbright : forall c, c <> [] -> pbbuild (map (fun x => (fst x, true :: snd x)) c) = pbright (pbbuild c).
proof: Proof. intros c; elim c; simpl in |- *; auto. intros H; case H; auto. intros a l; case a; case l. intros a0 l0 H H0; simpl in |- *; auto. intros p l0 a0 l1 H H0; rewrite H; auto. intros; discriminate. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)