proposition: Theorem pbfree_pbadd_prop1 : forall a1 l l1, ~ is_prefix l l1 -> ~ is_prefix l1 l -> pbfree l (pbadd a1 (pbleaf empty) l1).
proof: Proof. intros a1 l l1; generalize a1 l; elim l1; simpl in |- *; auto; clear a1 l l1. intros a1 l H H0; elim H0; auto. intros a; case a. intros l H a1 l0; case l0. intros H0; elim H0; auto. intros b; case b; simpl in |- *; auto. intros l1 H0 H1; apply pbfree_right2. apply H; auto. intros l H a1 l0; case l0; simpl in |- *; auto. intros H0; elim H0; auto. intros b; case b; simpl in |- *; auto. intros l1 H0 H1; apply pbfree_left2. apply H; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)