proposition: Theorem all_pbleaves_pbadd : forall l1 a1 a2 l, In a2 (all_pbleaves (pbadd a1 l l1)) -> a2 = a1 \/ In a2 (all_pbleaves l).
proof: Proof. intros l1; elim l1; simpl in |- *; auto. intros a1 a2 l [H| H]; auto; case H. intros a; case a. intros l H a1 a2 l0; case l0; simpl in |- *; auto. intros a0; elim l; simpl in |- *; auto. intuition. intros a3; case a3; simpl in |- *; auto. intros p H0; case in_app_or with (1 := H0); auto. elim l; simpl in |- *; auto. intuition. intros a3; case a3; simpl in |- *; auto. intros p p0 H0; case in_app_or with (1 := H0); auto with datatypes. intros H1; case H with (1 := H1); intuition auto with datatypes. intros l H a1 a2 l0; case l0; simpl in |- *; auto. intros a0; elim l; simpl in |- *; auto. intuition. intros a3; case a3; simpl in |- *; auto. intros p H0; case in_app_or with (1 := H0); auto. elim l; simpl in |- *; auto. intuition. intros a3; case a3; simpl in |- *; auto. intros p p0 H0; case in_app_or with (1 := H0); auto with datatypes. intros H1; case H with (1 := H1); intuition auto with datatypes. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)