proposition: Theorem insert_olist: forall a l, olist l -> olist (insert a l).
proof: Proof. intros a l; elim l; simpl; auto. intros; apply olist_one; auto. intros b l1 Rec H; case_eq (weight a b); intros H1; auto. apply olist_cons; auto. assert (Eq1: olist l1); try apply olist_inv with (1 := H). generalize (Rec Eq1). assert (Eq2: forall c, In c (insert a l1) -> weight b c = lt). intros c H2. case insert_inv with (1 := H2); auto. intros; subst; rewrite weight_anti_sym, H1; auto. intros H3; apply olist_weight with (1 := H); auto. generalize Eq2; case (insert a l1); auto. intros; apply olist_one. intros c l2 H2 H3; apply olist_cons; auto with datatypes. Qed.
imports: List Permutation UList