proposition: Theorem add_frequency_list_in_inv : forall (a1 a2 : A) (b1 : nat) l, In (a1, b1) (add_frequency_list a2 l) -> a1 = a2 \/ In (a1, b1) l.
proof: Proof. intros a1 a2 b1 l; elim l; simpl in |- *; auto. intros [H1| H1]; auto; injection H1; auto. intros (a3, b3) l1 Rec; simpl in |- *; auto. case (A_eq_dec a2 a3); simpl in |- *; auto. intros e H; cut (In (a1, b1) ((a2, S b3) :: l1)); auto. simpl in |- *; intros [H1| H1]; auto. injection H1; auto. intuition. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)