proposition: Theorem olist_skip: forall a b l, olist (a :: b :: l) -> olist (a :: l).
proof: Proof. intros a b l; generalize a b; elim l; simpl; auto. intros; apply olist_one. intros a1 l1 Rec a2 b1 H. assert (Eq1: weight a2 b1 = lt). inversion H; auto. assert (Eq2: weight b1 a1 = lt). inversion_clear H as [| H0 H1|]; auto. inversion_clear H1 ; auto. apply olist_cons; auto. rewrite weight_trans with (b := b1); auto. apply trans_equal with (1 := Eq1); auto. inversion_clear H; auto. inversion_clear H1; auto. Qed.
imports: List Permutation UList