proposition: Theorem pbbuild_pbnode : forall c1 c2, c1 <> [] -> c2 <> [] -> pbbuild (map (fun x => (fst x, false :: snd x)) c1 ++ map (fun x => (fst x, true :: snd x)) c2) = pbnode (pbbuild c1) (pbbuild c2).
proof: Proof. intros c1 c2 Hc1 Hc2; unfold pbbuild in |- *. rewrite fold_right_app. fold pbbuild in |- *. generalize pbbuild_true_pbright; unfold pbbuild in |- *; intros tmp; rewrite tmp; clear tmp; auto. generalize Hc1; elim c1; simpl in |- *; auto. intros H; case H; auto. intros a l; case a; case l; simpl in |- *; auto. intros p l0 a0 l1 H Hc0; rewrite H; auto. intros; discriminate. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)