proposition: Theorem insert_permutation : forall (L : list A) (a : A), Permutation (a :: L) (insert a L).
proof: Proof. intros L; elim L; simpl in |- *; auto. intros b l H' a. case_eq (order_fun a b); intros H1; auto. apply Permutation_trans with (l' := b :: a :: l); auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(Ordered)