proposition: Theorem add_frequency_list_perm : forall (a : A) l, Permutation (a :: flat_map (fun p => id_list (fst p) (snd p)) l) (flat_map (fun p => id_list (fst p) (snd p)) (add_frequency_list a l)).
proof: Proof. intros a l; generalize a; elim l; simpl in |- *; clear a l; auto. intros (a, n) l H b. case (A_eq_dec b a); auto. intros e; simpl in |- *; rewrite e; auto. simpl in |- *. intros e; apply Permutation_trans with (id_list a n ++ (b :: []) ++ flat_map (fun p => id_list (fst p) (snd p)) l); [ idtac | simpl in |- *; auto ]. change (Permutation ((b :: []) ++ id_list a n ++ flat_map (fun p => id_list (fst p) (snd p)) l) (id_list a n ++ (b :: []) ++ flat_map (fun p => id_list (fst p) (snd p)) l)) in |- *. repeat rewrite app_assoc; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)