proposition: Theorem add_frequency_list_unique_key : forall (a : A) l, unique_key l -> unique_key (add_frequency_list a l).
proof: Proof. intros a l; elim l; simpl in |- *; auto. intros (a1, n1) l1 Rec H; case (A_eq_dec a a1). intros e; apply unique_key_perm with (l1 := (a, S n1) :: l1); auto. apply unique_key_cons; auto. intros b; red in |- *; intros H0; case (unique_key_in _ _ _ _ b _ H); auto. rewrite <- e; auto. apply unique_key_inv with (1 := H); auto. intros n; apply unique_key_cons; auto. intros b; red in |- *; intros H0; case add_frequency_list_in_inv with (1 := H0); auto. intros H2; case (unique_key_in _ _ _ _ b _ H); auto. apply Rec; apply unique_key_inv with (1 := H); auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)