proposition: Theorem add_frequency_list_1 : forall a l, (forall ca, ~ In (a, ca) l) -> In (a, 1) (add_frequency_list a l).
proof: Proof. intros a l; generalize a; elim l; clear a l; simpl in |- *; auto. intros (a1, l1) l0 H a H0. case (A_eq_dec a a1); auto. intros H1; case (H0 l1); left; apply f_equal2 with (f := pair (A:=A) (B:=nat)); auto. intros n; apply in_cons; auto; apply H; auto. intros ca; red in |- *; intros H1; case (H0 ca); auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)