proposition: Theorem pbadd_prop1 : forall a1 a2 l1, compute_pbcode (pbadd a1 (pbleaf a2) l1) = (a1, l1) :: [].
proof: Proof. intros a1 a2 l1; generalize a1 a2; elim l1; simpl in |- *; auto; clear a1 a2 l1. intros a; case a; simpl in |- *; auto. intros l H a1 a2; rewrite H; simpl in |- *; auto. intros l H a1 a2; rewrite H; simpl in |- *; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)