proposition: Theorem pbfree_pbbuild_prop1 : forall a l1 l2, l2 <> [] -> unique_prefix ((a, l1) :: l2) -> pbfree l1 (pbbuild l2).
proof: Proof. intros a l1 l2; generalize a l1; elim l2; clear a l1 l2; simpl in |- *; auto. intros a l1 H; elim H; auto. intros (a1, l1) l; case l. unfold pbbuild in |- *; simpl in |- *; intros H a l0 H0 H1; apply pbfree_pbadd_prop1. red in |- *; intros H2; absurd (a = a1). red in |- *; intros H3; case unique_key_in with (a := a) (b1 := l0) (b2 := l1) (1 := unique_prefix2 _ _ H1); simpl in |- *; auto. rewrite H3; auto. apply unique_prefix1 with (1 := H1) (lb1 := l0) (lb2 := l1); simpl in |- *; auto. red in |- *; intros H2; absurd (a = a1). red in |- *; intros H3; case unique_key_in with (a := a) (b1 := l0) (b2 := l1) (1 := unique_prefix2 _ _ H1); simpl in |- *; auto. rewrite H3; auto. apply sym_equal; apply unique_prefix1 with (1 := H1) (lb1 := l1) (lb2 := l0); simpl in |- *; auto. intros p l0 H a l2 H0 H1. unfold pbbuild in |- *; simpl in |- *. apply pbfree_pbadd_prop2; auto. apply H with (a := a). red in |- *; intros; discriminate. apply unique_prefix_inv with (a := a1) (l := l1). apply unique_prefix_permutation with (2 := H1); auto. red in |- *; intros H2; absurd (a = a1). red in |- *; intros H3; case unique_key_in with (a := a) (b1 := l2) (b2 := l1) (1 := unique_prefix2 _ _ H1); simpl in |- *; auto. rewrite H3; auto. apply sym_equal; apply unique_prefix1 with (1 := H1) (lb1 := l1) (lb2 := l2); simpl in |- *; auto. red in |- *; intros H2; absurd (a = a1). red in |- *; intros H3; case unique_key_in with (a := a) (b1 := l2) (b2 := l1) (1 := unique_prefix2 _ _ H1); simpl in |- *; auto. rewrite H3; auto. apply unique_prefix1 with (1 := H1) (lb1 := l2) (lb2 := l1); simpl in |- *; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)