proposition: Theorem insert_ordered : forall l : list A, ordered order l -> forall a : A, ordered order (insert a l).
proof: Proof. Proof using order_fun_false order_fun_true. intros l H'; elim H'; clear H' l; auto. simpl in |- *; auto. intros a b; simpl in |- *. generalize (refl_equal (order_fun b a)); pattern (order_fun b a) at -1 in |- *; case (order_fun b a); intros Eq0; auto. intros a b l H'0 H'1 H'2 a0. simpl in |- *. generalize (refl_equal (order_fun a0 a)); pattern (order_fun a0 a) at -1 in |- *; case (order_fun a0 a); intros Eq0; auto. generalize (H'2 a0); simpl in |- *. generalize (refl_equal (order_fun a0 b)); pattern (order_fun a0 b) at -1 in |- *; case (order_fun a0 b); intros Eq1; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(Ordered)