proposition: Theorem add_frequency_list_in : forall m a n, unique_key m -> In (a, n) m -> In (a, S n) (add_frequency_list a m).
proof: Proof. intros m; elim m; clear m; simpl in |- *; auto. intros (a1, l1) l Rec a n H H1; case (A_eq_dec a a1); simpl in |- *; auto. intros H2; case H1; auto. intros H3; left; apply f_equal2 with (f := pair (A:=A) (B:=nat)); injection H3; auto. rewrite H2; intros H3; case unique_key_in with (1 := H) (b2 := n); auto. intros n0; right; apply Rec. apply unique_key_inv with (1 := H); auto. case H1; auto. intros H0; case n0; injection H0; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)