proposition: Theorem fold_pbadd_prop_left : forall l a, l <> [] -> fold_right (fun a (c : pbtree) => pbadd (fst a) c (snd a)) (pbleaf a) (map (fun v => match v with | (a1, b1) => (a1, false :: b1) end) l) = pbleft (fold_right (fun a (c : pbtree) => pbadd (fst a) c (snd a)) (pbleaf a) l).
proof: Proof. intros l; elim l. intros a H; elim H; simpl in |- *; auto. simpl in |- *; intros (a1, l1) l0; case l0. case l1; simpl in |- *; auto. intros p l2 H a H0. rewrite H; auto. red in |- *; intros H1; discriminate. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)