proposition: Theorem pbbuild_distinct_pbleaves : forall c, unique_prefix c -> distinct_pbleaves (pbbuild c).
proof: Proof. intros c; elim c; unfold pbbuild in |- *; simpl in |- *; auto. intros (a1, l1) l; case l; auto. simpl in |- *; intros H H0; apply distinct_pbleaves_pbadd_prop1; auto. intros (a2, l2) l3 H0 H1; apply distinct_pbleaves_pbadd_prop2; auto. change (~ inpb (pbleaf a1) (pbbuild ((a2, l2) :: l3))) in |- *. red in |- *; intros H2; case inpb_pbbuild_inv with (2 := H2). red in |- *; intros H; discriminate. intros x H; case unique_key_in with (b2 := x) (1 := unique_prefix2 _ _ H1); auto. apply H0. apply unique_prefix_inv with (1 := H1); auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)